]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/hbugs/tutors/search_pattern_apply_tutor.ml
mathql interpreter flags can be now red from helm registry
[helm.git] / helm / hbugs / tutors / search_pattern_apply_tutor.ml
index b410b604827b2d4c3e003dc5ce1ecc496385955d..0943dd1462244e3b19f87826bca944690b5f3bf8 100644 (file)
@@ -125,7 +125,6 @@ let dump_environment () =
   close_out oc
 
 let main () =
-  let mqi_flags = [] in (* default MathQL interpreter options *)
   try
     Sys.catch_break true;
     at_exit (fun () ->
@@ -135,7 +134,7 @@ let main () =
     broker_id :=
       Some (Hbugs_tutors_common.register_to_broker
         my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
-    let mqi_handle = MQIC.init mqi_flags prerr_string in 
+    let mqi_handle = MQIC.init prerr_string in 
     if Sys.file_exists environment_file then
       restore_environment ();
     Http_daemon.start'