aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Frontend.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2017-02-15 11:46:17 +0100
committerGitHub <noreply@github.com>2017-02-15 11:46:17 +0100
commit1aee802bf438fff7a83dec4607cabefdc398c3de (patch)
treee8e341b656c5e8ea6f61226878ad5dd1ee0e5082 /driver/Frontend.ml
parent53479577c06db853f48cf9927b5039507436be45 (diff)
parent5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb (diff)
downloadcompcert-1aee802bf438fff7a83dec4607cabefdc398c3de.tar.gz
compcert-1aee802bf438fff7a83dec4607cabefdc398c3de.zip
Merge pull request #167 from AbsInt/pipe_prerequisite
Introduced configuration variable for gnu systems.
Diffstat (limited to 'driver/Frontend.ml')
-rw-r--r--driver/Frontend.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 41ca3bb8..b4b161b0 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -125,7 +125,7 @@ let prepro_actions = [
Exact "-Xpreprocessor", String (fun s ->
prepro_options := s :: !prepro_options);
Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options);]
- @ (if gnu_system then gnu_prepro_actions else [])
+ @ (if Configuration.gnu_toolchain then gnu_prepro_actions else [])
let gnu_prepro_help =
{| -M Ouput a rule suitable for make describing the
@@ -163,4 +163,4 @@ let prepro_help = {|Preprocessing options:
-Wp,<opt> Pass option <opt> to the preprocessor
-Xpreprocessor <opt> Pass option <opt> to the preprocessor
|}
- ^ (if gnu_system then gnu_prepro_help else "")
+ ^ (if Configuration.gnu_toolchain then gnu_prepro_help else "")