From a7d8c13a2309ca4de1b786c8eec14ea9d1e19d3c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Jul 2005 08:37:54 +0000 Subject: [PATCH] renamed development related windows --- helm/matita/matita.glade | 4 ++-- helm/matita/matitaGui.ml | 2 +- helm/matita/matitaGui.mli | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index b246c91aa..1076b9192 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -3184,7 +3184,7 @@ - + Create development GTK_WINDOW_TOPLEVEL GTK_WIN_POS_CENTER_ALWAYS @@ -3410,7 +3410,7 @@ - + Developments GTK_WINDOW_TOPLEVEL GTK_WIN_POS_CENTER diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 6cc4731ad..a41215bd4 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -110,7 +110,7 @@ class gui () = let fileSel = new fileSelectionWin () in let findRepl = new findReplWin () in let develList = new develListWin () in - let newDevel = new newDevelopmentWin () in + let newDevel = new newDevelWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] in diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index a2b15513e..0943862ce 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -52,7 +52,7 @@ object method main : MatitaGeneratedGui.mainWin method findRepl : MatitaGeneratedGui.findReplWin method develList: MatitaGeneratedGui.develListWin - method newDevel: MatitaGeneratedGui.newDevelopmentWin + method newDevel: MatitaGeneratedGui.newDevelWin (* method toolbar : MatitaGeneratedGui.toolBarWin *) method console: console -- 2.39.2