diff options
| author | Jan Holthuis <jan.holthuis@ruhr-uni-bochum.de> | 2021-04-11 16:36:17 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-11 16:36:17 +0200 |
| commit | 820889b9210e922ae85c1264ff2815d7e81b5464 (patch) | |
| tree | 59b6eed885c1e3bfda73873e05f2b23eb8322e92 /script | |
| parent | 1cdf0321249f244f08ed51d80a1346c786e59755 (diff) | |
| parent | 895a485fa88221ce7afe8edbdb605a51a9fa07dd (diff) | |
Merge pull request #3778 from JoergAtGithub/2.3_windows_local_buildfix
Fixed build settings for local Windows development environment
Diffstat (limited to 'script')
0 files changed, 0 insertions, 0 deletions