diff options
| -rwxr-xr-x | test-suite/check | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 9 |
2 files changed, 8 insertions, 5 deletions
diff --git a/test-suite/check b/test-suite/check index 91007ef45d..99893f8826 100755 --- a/test-suite/check +++ b/test-suite/check @@ -8,7 +8,7 @@ else coqtop="../bin/coqtop -q -batch" fi -command="$coqtop -load-vernac-source" +command="$coqtop -top Top -load-vernac-source" # on compte le nombre de tests et de succès nbtests=0 @@ -20,7 +20,7 @@ test_success() { for f in $1/*.v; do nbtests=`expr $nbtests + 1` printf " "$f"..." - $command $f $2 > /dev/null 2>&1 + $command $f $2 > /dev/null 2>&1 if [ $? = 0 ]; then echo "Ok" nbtestsok=`expr $nbtestsok + 1` diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 97ba5c81cf..c55568b3a7 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -50,8 +50,11 @@ let engage () = let set_batch_mode () = batch_mode := true -let toplevel_name = ref (make_dirpath [id_of_string "Top"]) +let toplevel_name = ref None +let toplevel_default_name = make_dirpath [id_of_string "Top"] let set_toplevel_name dir = toplevel_name := dir +let get_toplevel_name () = + match !toplevel_name with Some dir -> dir | None -> toplevel_default_name let remove_top_ml () = Mltop.remove () @@ -310,8 +313,8 @@ let init is_ide = inputstate (); set_vm_opt (); engage (); - if not !batch_mode && Global.env_is_empty() then - Declaremods.start_library !toplevel_name; + if (not !batch_mode|| !toplevel_name<>None) && Global.env_is_empty() then + Declaremods.start_library (get_toplevel_name ()) init_library_roots (); load_vernac_obj (); require (); |