From: Claudio Sacerdoti Coen Date: Sat, 22 Dec 2018 00:09:10 +0000 (+0100) Subject: findReplace ported from GtkTable to GtkGrid X-Git-Tag: make_still_working~229^2~25 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1c8e7170469dd7859fcf15dc76b3162d494cd848;p=helm.git findReplace ported from GtkTable to GtkGrid --- diff --git a/matita/matita/matita.ui b/matita/matita/matita.ui index 47987930e..f1f674ec1 100644 --- a/matita/matita/matita.ui +++ b/matita/matita/matita.ui @@ -139,7 +139,6 @@ True False - horizontal False @@ -172,7 +171,6 @@ 4 4 end - horizontal gtk-media-pause @@ -1081,12 +1079,10 @@ mouse dialog - + True False - 3 - 2 - 5 + 9 True @@ -1095,8 +1091,8 @@ 0 - - + 0 + 0 @@ -1107,24 +1103,20 @@ 0 + 0 1 - 2 - - True True - True True True 1 - 2 - + 0 @@ -1134,10 +1126,7 @@ 1 - 2 1 - 2 - @@ -1145,18 +1134,7 @@ True False 5 - - - True - False - vertical - - - True - True - 0 - - + True gtk-find @@ -1239,10 +1217,9 @@ - 2 + 0 2 - 3 - 5 + 2 @@ -1763,7 +1740,6 @@ True True - horizontal True @@ -2213,6 +2189,11 @@ + + False + True + 0 + @@ -2449,8 +2430,8 @@ 500 True True - 380 vertical + 380 True