aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-07-01 17:25:44 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-07-01 17:25:44 +0200
commitb59b2b182a6832e1b6ebf3cf7ba4fd1943843b74 (patch)
tree3fa8c338c917d4f72f3408b6a45cffcc6e1e0f8a /driver/Configuration.ml
parentd8ed56833c508b5103a900ef04975013bd9ba77b (diff)
downloadcompcert-b59b2b182a6832e1b6ebf3cf7ba4fd1943843b74.tar.gz
compcert-b59b2b182a6832e1b6ebf3cf7ba4fd1943843b74.zip
Removed the version from the compcert.ini file and add it again in a separate file.
Diffstat (limited to 'driver/Configuration.ml')
-rw-r--r--driver/Configuration.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 70131fc6..64f24820 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -104,7 +104,6 @@ let advanced_debug =
| "false" -> false
| v -> bad_config "advanced_debug" [v]
-let version = get_config_string "version"
type struct_passing_style =
| SP_ref_callee (* by reference, callee takes copy *)