]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matitac.ml
get rid of gragrep, matitamake(Lib) and development windows,
[helm.git] / matita / matitac.ml
index 8645d21755ca4460c9747715ad5c024e2a53de86..8f8a19b2da8c94e43082b54b6ec02497d1d76a4f 100644 (file)
@@ -145,12 +145,9 @@ let main_compiler () =
 let main () =
  Helm_registry.set_bool "matita.moo" true;
  match Filename.basename Sys.argv.(0) with
- |"gragrep"    |"gragrep.opt"    |"gragrep.opt.static"    ->Gragrep.main()
  |"matitadep"  |"matitadep.opt"  |"matitadep.opt.static"  ->Matitadep.main()
  |"matitaclean"|"matitaclean.opt"|"matitaclean.opt.static"->Matitaclean.main()
- |"matitamake" |"matitamake.opt" |"matitamake.opt.static" ->Matitamake.main()
- |"matitaprover"|"matitaprover.opt"
- |"matitaprover.opt.static" ->Matitaprover.main()
+ |"matitaprover"|"matitaprover.opt"|"matitaprover.opt.static"->Matitaprover.main()
  |"matitawiki"|"matitawiki.opt" ->MatitaWiki.main()
  | _ ->
     let dump_msg = "<filename> Dump with expanded macros to <filename>" in