summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-30 12:19:52 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-30 12:19:52 +0000
commit66cb2a32e2321d1d0c244623b3a9cb8274d203f3 (patch)
treea72596b33d150d47be8186f9de503ff1dfba73a3
parent40141e6651bf02ef56d35bd6b3e64e4445d1593f (diff)
Options -I -D -U with a space
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--driver/Driver.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index d7c9364..255b600 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -294,6 +294,9 @@ let cmdline_actions =
let f_opt name ref =
["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in
[
+ "-I$", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
+ "-D$", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
+ "-U$", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
"-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options);
"-[lL].", Self(fun s -> linker_options := s :: !linker_options);
"-o$", String(fun s -> exe_name := s);