From 66cb2a32e2321d1d0c244623b3a9cb8274d203f3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Mar 2010 12:19:52 +0000 Subject: Options -I -D -U with a space git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Driver.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'driver') 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); -- cgit