aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorMichael Schmidt <github@mschmidt.me>2015-12-23 12:12:17 +0100
committerMichael Schmidt <github@mschmidt.me>2015-12-23 12:12:17 +0100
commit381d957b4d1439b0d6da8ef4d118945f88381e4c (patch)
treead4b96847c9a53700945b87d9c80cd902bdd7f44 /driver/Driver.ml
parent7a8558575054daff45d41bdfe4058596f87467a3 (diff)
downloadcompcert-381d957b4d1439b0d6da8ef4d118945f88381e4c.tar.gz
compcert-381d957b4d1439b0d6da8ef4d118945f88381e4c.zip
add options for include paths also to the command line of the assembler, bug 17838
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index db3031b4..8509e84a 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -533,8 +533,10 @@ let cmdline_actions =
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);
+ Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options;
+ assembler_options := s :: "-I" :: !assembler_options);
+ Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options;
+ assembler_options := s :: !assembler_options);
Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options);
Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);