diff mkoctfile.cc.in @ 9957:59ed11557715

mkoctfile: if output file is specified and it does not end in output_ext, append output_ext
author John W. Eaton <jwe@octave.org>
date Thu, 10 Dec 2009 02:09:53 -0500
parents f26a33e21db9
children 4906ccf5d95e
line wrap: on
line diff
--- a/mkoctfile.cc.in	Thu Dec 10 01:49:15 2009 -0500
+++ b/mkoctfile.cc.in	Thu Dec 10 02:09:53 2009 -0500
@@ -570,7 +570,13 @@
   else
     {
       if (!outputfile.empty ())
-	octfile = outputfile;
+        {
+          octfile = outputfile;
+          size_t len = octfile.length ();
+          size_t len_ext = output_ext.length ();
+          if (octfile.substr (len-len_ext) != output_ext)
+            octfile += output_ext;
+        }
       else
 	octfile = basename (octfile, true) + output_ext;
     }