]> matita.cs.unibo.it Git - helm.git/commit
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
tree169568fc0c47bb8008b43ea375200f0e8b9c9c70
parent57f19e78a66217588b6f097f378211b7c2890857
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