diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-19 09:44:26 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-19 09:44:26 +0200 |
commit | 2129fe8f2e19c4dd91955e5300e76d924e0a3e6d (patch) | |
tree | 142db2c4fd4931dc7b2d6cfb1bf77e8f4e5ec584 /driver/Frontend.ml | |
parent | efa462bd1655c6b2c8f064e214762650092257e8 (diff) | |
download | compcert-2129fe8f2e19c4dd91955e5300e76d924e0a3e6d.tar.gz compcert-2129fe8f2e19c4dd91955e5300e76d924e0a3e6d.zip |
Merged responfile function into command.
Command now decides whether to use a responsefile or call the
external command directly.
Bug 18004
Diffstat (limited to 'driver/Frontend.ml')
-rw-r--r-- | driver/Frontend.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 41b09b58..043d4e5a 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -24,11 +24,8 @@ open Printf let preprocess ifile ofile = let output = if ofile = "-" then None else Some ofile in - let cmd,opts = match Configuration.prepro with - | name::opts -> name,opts - | [] -> assert false (* Should be catched in Configuration *) in - let opts = List.concat [ - opts; + let cmd = List.concat [ + Configuration.prepro; ["-D__COMPCERT__"]; (if !Clflags.use_standard_headers then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ] @@ -36,8 +33,6 @@ let preprocess ifile ofile = List.rev !prepro_options; [ifile] ] in - let opts = responsefile opts (fun a -> if gnu_system then ["@"^a] else ["@"^a]) in - let cmd = cmd::opts in let exc = command ?stdout:output cmd in if exc <> 0 then begin if ofile <> "-" then safe_remove ofile; |