2019-07-19 | jenkins | Merge branch 'release/5.8.0' 5.8.0 | blob | commitdiff | raw |
2019-06-04 | Katja Luther | merge hotfix5.7.3 into develop | blob | commitdiff | raw |
2019-05-27 | Katja Luther | ref #8045: further implementation for default/explicit... | blob | commitdiff | raw |
2019-05-06 | jenkins | Merge branch 'release/5.7.0' into develop | blob | commitdiff | raw | diff to current |
2019-05-06 | Katja Luther | ref #8045: show possible entries for preferences in... | blob | commitdiff | raw | diff to current |
2018-05-17 | jenkins | Merge branch 'release/5.0.0' 5.0.0 | blob | commitdiff | raw | diff to current |
2018-02-15 | Patrick Plitzner | ref #7268 Implement own extension point for preferences | blob | commitdiff | raw | diff to current |