aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Clflags.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2016-05-27 09:02:40 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2016-05-27 09:02:40 +0200
commitb45cdb9dce7df376fd3cb27a32863af90b847b78 (patch)
tree03ceac74e5bf28a4d3bed7167c863ffff9c14a54 /driver/Clflags.ml
parent672393ef623acb3e230a8019d51c87e051a7567a (diff)
parent8c28d0630576de35e739edebc2abe127d18de22a (diff)
downloadcompcert-b45cdb9dce7df376fd3cb27a32863af90b847b78.tar.gz
compcert-b45cdb9dce7df376fd3cb27a32863af90b847b78.zip
Merge pull request #100 from AbsInt/driver-split
Driver refactoring
Diffstat (limited to 'driver/Clflags.ml')
-rw-r--r--driver/Clflags.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 394dc448..6a695aa4 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -61,3 +61,5 @@ let option_small_data =
let option_small_const = ref (!option_small_data)
let option_timings = ref false
let option_rename_static = ref false
+let stdlib_path = ref Configuration.stdlib_path
+let use_standard_headers = ref Configuration.has_standard_headers