diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-30 12:19:52 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-30 12:19:52 +0000 |
| commit | 66cb2a32e2321d1d0c244623b3a9cb8274d203f3 (patch) | |
| tree | a72596b33d150d47be8186f9de503ff1dfba73a3 | |
| parent | 40141e6651bf02ef56d35bd6b3e64e4445d1593f (diff) | |
| download | compcert-kvx-66cb2a32e2321d1d0c244623b3a9cb8274d203f3.tar.gz compcert-kvx-66cb2a32e2321d1d0c244623b3a9cb8274d203f3.zip | |
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.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index d7c93641..255b6004 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); |