merge with dev

2019-04-16 10:59:38 +02:00
parent 55d96fca51 7d33fc40cd
commit c9af6109ab
12 changed files with 59 additions and 34 deletions
--- a/rtgui/preferences.h
+++ b/rtgui/preferences.h
@@ -145,6 +145,8 @@ class Preferences : public Gtk::Dialog, public ProfileStoreListener
    Gtk::FontButton* colorPickerFontFB;
    Gtk::ColorButton* cropMaskColorCB;
    Gtk::ColorButton* navGuideColorCB;
+    Gtk::CheckButton* pseudoHiDPI;
+

    Gtk::SpinButton*   maxRecentFolders;
    Gtk::SpinButton*   maxThumbHeightSB;