Merge branch 'master' into dev

2026-07-22 09:54:27 +00:00 · 2019-09-04 15:50:18 +02:00
parent 642442c977 326eb5e343
commit 570bec299f
20 changed files with 1033 additions and 1093 deletions
@@ -720,6 +720,9 @@ public:
        const wxString& name = wxEmptyString);
    ~DoubleSlider() {}

+    // permissible error for layer height
+    static double epsilon() { return 0.0011;}
+
    void    msw_rescale();

    int GetMinValue() const { return m_min_value; }