ui.tools.workspace: Add workspace-dim global variable
							parent
							
								
									28ee96af40
								
							
						
					
					
						commit
						b7191f3706
					
				|  | @ -69,7 +69,11 @@ M: gadget tool-scroller drop f ; | ||||||
|     [ find-workspace hide-popup ] <debugger> |     [ find-workspace hide-popup ] <debugger> | ||||||
|     "Error" show-titled-popup ; |     "Error" show-titled-popup ; | ||||||
| 
 | 
 | ||||||
| M: workspace pref-dim* drop { 600 700 } ; | SYMBOL: workspace-dim | ||||||
|  | 
 | ||||||
|  | { 600 700 } workspace-dim set-global | ||||||
|  | 
 | ||||||
|  | M: workspace pref-dim* drop workspace-dim get ; | ||||||
| 
 | 
 | ||||||
| M: workspace focusable-child* | M: workspace focusable-child* | ||||||
|     dup workspace-popup [ ] [ workspace-listener ] ?if ; |     dup workspace-popup [ ] [ workspace-listener ] ?if ; | ||||||
|  |  | ||||||
		Loading…
	
		Reference in New Issue