Hi, Ignacio Casal Quinteiro changed devhelp to use GdHeaderBar (in place of GdMainToolbar); this improves the styling and allows to drag the header bar to move the window.
This is minor but it improves consistency with other apps, I'd like to request an exception to land this is, https://git.gnome.org/browse/devhelp/commit/?h=wip/headerbar Thanks, Fred _______________________________________________ release-team@gnome.org https://mail.gnome.org/mailman/listinfo/release-team Release-team lurker? Do NOT participate in discussions.
