]> matita.cs.unibo.it Git - helm.git/commitdiff
now should run also when the db is down (untested)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 9 Sep 2004 16:36:46 +0000 (16:36 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 9 Sep 2004 16:36:46 +0000 (16:36 +0000)
(the -nodb option is still unimplemented)

helm/gTopLevel/gTopLevel.ml

index 197b6f1ee305b6db4d121934f19f228bd8d57795..ba0615246050989f471374ef9310d0283f755311 100644 (file)
@@ -62,7 +62,7 @@ let _ =
 (* GLOBAL CONSTANTS *)
 
 let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_handle = MQIC.init ~log:mqi_debug_fun ()
+let mqi_handle = MQIC.init_if_connected ~log:mqi_debug_fun ()
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;