X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;ds=inline;f=src%2Fui%2Fgui%2Foutput-window.ui;h=a8aa42db42ec7b404c4063c850cbe68dd83c9fca;hb=c2d972816fce591524db963390a97ff32d55117c;hp=f89deb10c447951abc076c9b4182bcbcaba6258c;hpb=58c32883c1675879e1d59f703033af702e214040;p=pspp
diff --git a/src/ui/gui/output-window.ui b/src/ui/gui/output-window.ui
index f89deb10c4..a8aa42db42 100644
--- a/src/ui/gui/output-window.ui
+++ b/src/ui/gui/output-window.ui
@@ -15,7 +15,7 @@
file-print
_Print...
-
+
edit-copy
edit_copy
- _Copy
+ _Copy
@@ -52,7 +52,7 @@
- windows-minimize-all
+ windows-minimize-all
windows_minimise-all
_Minimize All Windows
@@ -77,77 +77,71 @@
-
+
+ True
+ GTK_ORIENTATION_VERTICAL
GDK_POINTER_MOTION_MASK | GDK_POINTER_MOTION_HINT_MASK | GDK_BUTTON_PRESS_MASK | GDK_BUTTON_RELEASE_MASK
- 600
- 400
-
+
+
+ False
+ 0
+
+
+
+
+ True
+ GTK_ORIENTATION_HORIZONTAL
+ True
+ 112
+ True
-
-
+
True
- GTK_ORIENTATION_HORIZONTAL
True
- 112
- True
-
-
- True
- True
- automatic
- automatic
-
-
- True
- True
- False
-
-
-
-
- False
- True
-
-
+ GDK_POINTER_MOTION_MASK | GDK_POINTER_MOTION_HINT_MASK | GDK_BUTTON_PRESS_MASK | GDK_BUTTON_RELEASE_MASK
+ automatic
+ automatic
-
+
True
- True
+ 5
GDK_POINTER_MOTION_MASK | GDK_POINTER_MOTION_HINT_MASK | GDK_BUTTON_PRESS_MASK | GDK_BUTTON_RELEASE_MASK
- automatic
- automatic
-
-
- True
- GDK_POINTER_MOTION_MASK | GDK_POINTER_MOTION_HINT_MASK | GDK_BUTTON_PRESS_MASK | GDK_BUTTON_RELEASE_MASK
-
-
-
- True
- True
-
- 1
- True
+ True
+ True
+
+ 1
+ True
+