From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 23 Dec 2010 22:14:44 +0000 (+0000)
Subject: Bug fixed (introduced in previous commit): opening multiple files requires first
X-Git-Tag: make_still_working~2621
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a9afd40d8d1b517a474afe7dcb77197831b1bd75;p=helm.git

Bug fixed (introduced in previous commit): opening multiple files requires first
the creation of the newScript to be replaced.
---

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index 9ea693344..94a34570a 100644
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -112,10 +112,8 @@ let _ =
   let args = Helm_registry.get_list Helm_registry.string "matita.args" in
   let gui = MatitaGui.instance () in
   init_debugging_menu gui;
-  if args = [] then
-   gui#newScript ()
-  else
-   List.iter gui#loadScript (List.rev args);
+  gui#newScript ();
+  List.iter gui#loadScript (List.rev args);
   gui#main#mainWin#show ();
   try
    GtkThread.main ()