X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Foutput-window.ui;h=a8aa42db42ec7b404c4063c850cbe68dd83c9fca;hb=03a7b96a587a58bda342b4eb5ce5f935880ba2b7;hp=a9b7702e5b6a62b933736cb2dae17290f1aa18da;hpb=0df9cdd3df66caf4353128feff3008289cda8115;p=pspp
diff --git a/src/ui/gui/output-window.ui b/src/ui/gui/output-window.ui
index a9b7702e5b..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,74 +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
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
+
+ 1
+ True
+