]> matita.cs.unibo.it Git - helm.git/commitdiff
Dead dialog window removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Oct 2006 13:17:10 +0000 (13:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Oct 2006 13:17:10 +0000 (13:17 +0000)
matita/matitaGuiTypes.mli

index 6457dc0c8d5701cac8d06a58582fe96653f85814..67d431040df41af64635e4f4e501c9e57d9cd114 100644 (file)
@@ -62,7 +62,6 @@ object
 
   method newBrowserWin:         unit -> browserWin
   method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
-  method newRecordDialog:       unit -> MatitaGeneratedGui.recordChoiceDialog
   method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
   method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog