aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-10-06 18:53:58 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2014-10-06 18:53:58 +0200
commit64faa3f42647da25c69941053211492b7f74a35d (patch)
treef84d1fac316cf8c31427c3840c76eeb61f7ad8dc /driver/Driver.ml
parenta2bed030e01bfe6e3addbe44f724de5c5fbeab65 (diff)
downloadcompcert-64faa3f42647da25c69941053211492b7f74a35d.tar.gz
compcert-64faa3f42647da25c69941053211492b7f74a35d.zip
Removed environment variable for the stdlib_path and added a new variable for the configuration file.
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml6
1 files changed, 1 insertions, 5 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 7dacc4d2..18005302 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -17,11 +17,7 @@ open Timing
(* Location of the compatibility library *)
-let stdlib_path = ref(
- try
- Sys.getenv "COMPCERT_LIBRARY"
- with Not_found ->
- Configuration.stdlib_path)
+let stdlib_path = ref Configuration.stdlib_path
let command cmd =
if !option_v then begin