]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/matitaGui.ml
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 57f19e7) | patch
Bug fixed: the newScript method must be called only after registering the
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 11 Jan 2011 22:02:11 +0000 (22:02 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 11 Jan 2011 22:02:11 +0000 (22:02 +0000)
commit591098895b69f9179c6156cac43abdf0d38a8708
tree169568fc0c47bb8008b43ea375200f0e8b9c9c70tree | snapshot
parent57f19e78a66217588b6f097f378211b7c2890857commit | diff
Bug fixed: the newScript method must be called only after registering the
gui. I have moved the invocation of self#newScript from the initializer to the
instance() function to solve the issue (an ugly gtk error when Matita starts).
matita/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.