ui.tools.browser: don't scroll up when reloading page
parent
c52ffebffe
commit
9159ce74ab
|
@ -83,8 +83,8 @@ M: browser-gadget handle-gesture
|
||||||
} 2|| ;
|
} 2|| ;
|
||||||
|
|
||||||
M: browser-gadget definitions-changed ( assoc browser -- )
|
M: browser-gadget definitions-changed ( assoc browser -- )
|
||||||
model>> [ value>> swap showing-definition? ] keep
|
[ model>> value>> swap showing-definition? ] keep
|
||||||
'[ _ notify-connections ] when ;
|
'[ _ [ history-value ] keep set-history-value ] when ;
|
||||||
|
|
||||||
M: browser-gadget focusable-child* search-field>> ;
|
M: browser-gadget focusable-child* search-field>> ;
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue