From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Oct 2010 12:00:11 +0000 (+0000)
Subject: Bug fixed: it always made an undo to the empty status (stupid bug
X-Git-Tag: make_still_working~2771
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9072df10d7f7db0348c3a23f8aa324ba262600d9;p=helm.git

Bug fixed: it always made an undo to the empty status (stupid bug
introduced in last commit)
---

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index f3656081f..3ab92575c 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -429,8 +429,7 @@ object (self)
     match history with s::_ -> s | [] -> assert false
    in
     LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
-    NCicLibrary.time_travel
-     ((new GrafiteTypes.status cur_grafite_status#baseuri)#set_lstatus cur_grafite_status#lstatus);
+    NCicLibrary.time_travel grafite_status;
     statements <- new_statements;
     history <- new_history;
     self#moveMark (- offset)