]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaInit.ml
new tacticals
[helm.git] / helm / matita / matitaInit.ml
index 84dff49e9eced28ba3de448426503fc6550f0d56..e69c22cf87a7897f36c1c071df9c6e4c221a37d0 100644 (file)
@@ -149,10 +149,12 @@ let usage () =
   try Hashtbl.find usages usage_key with Not_found -> default_usage
 
 let registry_defaults =
-  [ "matita.debug", "false";
-    "matita.quiet", "false";
-    "matita.preserve", "false";
-    "db.nodb", "false";
+  [
+    "db.nodb",                  "false";
+    "matita.debug",             "false";
+    "matita.external_editor",   "gvim -f -c 'go %p' %f";
+    "matita.preserve",          "false";
+    "matita.quiet",             "false";
   ]
 
 let set_registry_values =