aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-05-31 20:00:24 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-05-31 20:00:24 +0200
commit6ae45c3aa11d0c70b83b6b7e91a784b23a67146d (patch)
tree0719bdb02e8820c5c8b0e2c74a42f98af0f25d85
parentef16a51223a4b73eed74c40ce9938248ab6b4b8a (diff)
downloadcompcert-kvx-6ae45c3aa11d0c70b83b6b7e91a784b23a67146d.tar.gz
compcert-kvx-6ae45c3aa11d0c70b83b6b7e91a784b23a67146d.zip
Allow the option -o to be also the prefix of the file name for compability with different build systems.
-rw-r--r--driver/Driver.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index d225ec4f..aaaeb5b5 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -502,6 +502,8 @@ let cmdline_actions =
Exact "-E", Set option_E;
Exact "-S", Set option_S;
Exact "-o", String(fun s -> option_o := Some s);
+ Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in
+ option_o := Some s);
(* Preprocessing options *)
Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options);