]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matitac.ml
modifications to make matita behave reasonably, removed some useless windows
[helm.git] / matita / matitac.ml
index 868326a8dec808c68d1781bea0b3191d83f81d50..8645d21755ca4460c9747715ad5c024e2a53de86 100644 (file)
@@ -135,17 +135,7 @@ let main_compiler () =
         with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
       ;;
   
-      let build fname = 
-        let oldfname = 
-          Helm_registry.get_opt
-           Helm_registry.string "matita.filename"
-        in
-        let rc = MatitacLib.compile fname in
-        (match oldfname with
-        | Some n -> Helm_registry.set_string "matita.filename" n;
-        | _ -> Helm_registry.unset "matita.filename");
-        rc
-      ;;
+      let build = MatitacLib.compile;;
     end 
   in
   let module Make = Make.Make(F) in