Removed environment variable for the stdlib_path and added a new variable for the configuration file.

Author: bschommer

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

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

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.     *)
 (*                                                                     *)
 (* *********************************************************************)