Options -I -D -U with a space

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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);