From 64faa3f42647da25c69941053211492b7f74a35d Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 6 Oct 2014 18:53:58 +0200
Subject: Removed environment variable for the stdlib_path and added a new
 variable for the configuration file.

---
 driver/Configuration.ml | 26 +++++++++++++++-----------
 driver/Driver.ml        |  6 +-----
 driver/Timing.ml        |  8 ++++----
 3 files changed, 20 insertions(+), 20 deletions(-)

(limited to 'driver')

diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index c4bcf278..1956b151 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -18,18 +18,22 @@ let config_vars: (string, string) Hashtbl.t = Hashtbl.create 10
 let _ =
   try
     let file = 
-      let dir = Sys.getcwd () 
-      and name = Sys.argv.(0) in
-      let dirname = if Filename.is_relative name then
-        Filename.dirname (Filename.concat dir name)
-      else 
-        Filename.dirname name
-      in
-      let share_dir = Filename.concat (Filename.concat dirname Filename.parent_dir_name) "share" in
       try
-        open_in (Filename.concat dirname "compcert.ini")
-      with Sys_error _ ->
-        open_in (Filename.concat share_dir "compcert.ini")
+        let env_file = Sys.getenv "COMPCERT_CONFIG" in
+        open_in env_file
+      with Not_found ->
+        let dir = Sys.getcwd () 
+        and name = Sys.argv.(0) in
+        let dirname = if Filename.is_relative name then
+          Filename.dirname (Filename.concat dir name)
+        else 
+          Filename.dirname name
+        in
+        let share_dir = Filename.concat (Filename.concat dirname Filename.parent_dir_name) "share" in
+        try
+          open_in (Filename.concat dirname "compcert.ini")
+        with Sys_error _ ->
+          open_in (Filename.concat share_dir "compcert.ini")
     in
     (try
       let ini_line = Str.regexp "\\([^=]+\\)=\\(.+\\)" in
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
diff --git a/driver/Timing.ml b/driver/Timing.ml
index b45dad40..f660e9c7 100644
--- a/driver/Timing.ml
+++ b/driver/Timing.ml
@@ -2,11 +2,11 @@
 (*                                                                     *)
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
-(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
 (*                                                                     *)
-(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
-(*  is distributed under the terms of the INRIA Non-Commercial         *)
-(*  License Agreement.                                                 *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
 (*                                                                     *)
 (* *********************************************************************)
 
-- 
cgit