From e292f758f7ee489815603db7ff0b3bba7602ddeb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 18 Oct 2006 13:17:10 +0000 Subject: [PATCH] Dead dialog window removed. --- matita/matitaGuiTypes.mli | 1 - 1 file changed, 1 deletion(-) diff --git a/matita/matitaGuiTypes.mli b/matita/matitaGuiTypes.mli index 6457dc0c8..67d431040 100644 --- a/matita/matitaGuiTypes.mli +++ b/matita/matitaGuiTypes.mli @@ -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 -- 2.39.2