]> matita.cs.unibo.it Git - helm.git/commit
disambiguationErrors now uses #run
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 24 Dec 2018 00:05:41 +0000 (01:05 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 24 Dec 2018 00:05:41 +0000 (01:05 +0100)
commit3621e248131c72d46d5babe1c403af0712f2511a
treed8e0c7ed56ab9a33c5b9c70a4c31e6a207a9e75c
parent597e5f42a14179dc0b4811046c622dd85944897b
disambiguationErrors now uses #run

correct Gtk behavior
matita/matita/matitaGui.ml