hi all,
for the archive:
gui/workspace.py =
# Edge bumping
# Bump the mouse into the edge of the screen to get back the stuff
# that was hidden there, similar to media players etc.
edges = self._get_bumped_edges(widget, event)
if not edges:
self._start_autohide_timeout()
return False
if edges & self._EDGE_TOP and self.header_bar:
pass
#self.header_bar.show_all()
if edges & self._EDGE_BOTTOM and self.footer_bar:
pass
#self.footer_bar.show_all()
if edges & self._EDGE_LEFT and not self._lstack.is_empty():
pass
#self._lscrolls.show_all()
if edges & self._EDGE_RIGHT and not self._rstack.is_empty():
pass
#self._rscrolls.show_all()
but i am still not sure if there's an option in mypaint / preferences
to avoid this modification.
cheers
_______________________________________________
Mypaint-discuss mailing list
[email protected]
https://mail.gna.org/listinfo/mypaint-discuss
