X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Foutput-window.ui;h=1a1a02f9405e4b4067f781cfd8ad00a4f5155f63;hb=0cd7c010e3e5c316ef0eb0317fb7f408d164679d;hp=3c9686d566ed657466c76b1aa4c917b42dc3a5b5;hpb=1c492427c0c4e03065f4a327549a6d31b9e693a8;p=pspp diff --git a/src/ui/gui/output-window.ui b/src/ui/gui/output-window.ui index 3c9686d566..1a1a02f940 100644 --- a/src/ui/gui/output-window.ui +++ b/src/ui/gui/output-window.ui @@ -15,7 +15,7 @@ file-print _Print... - + @@ -34,27 +34,14 @@ edit_select-all edit-select-all - Select _All + Select _All edit-copy edit_copy - _Copy - - - - - windows_menuitem - _Windows - - - - - windows-minimize-all - windows_minimise-all - _Minimize All Windows + _Copy @@ -69,79 +56,76 @@ - - - - + + True + GTK_ORIENTATION_VERTICAL + GDK_POINTER_MOTION_MASK | GDK_POINTER_MOTION_HINT_MASK | GDK_BUTTON_PRESS_MASK | GDK_BUTTON_RELEASE_MASK + + True - GTK_ORIENTATION_VERTICAL GDK_POINTER_MOTION_MASK | GDK_POINTER_MOTION_HINT_MASK | GDK_BUTTON_PRESS_MASK | GDK_BUTTON_RELEASE_MASK + + + False + 0 + + + + + True + GTK_ORIENTATION_HORIZONTAL + True + 112 + True - + True - GDK_POINTER_MOTION_MASK | GDK_POINTER_MOTION_HINT_MASK | GDK_BUTTON_PRESS_MASK | GDK_BUTTON_RELEASE_MASK + True + automatic + automatic + + + True + True + False + + - False - 0 + False + 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 - 5 - 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 + + +