| commit | a8d47c3c71767414add8177b538f1783528f5cd6 | |
| author | Mikolaj Konarski <mikolaj@well-typed.com> | |
| Sat, 7 Aug 2021 21:41:46 +0000 (7 23:41 +0200) | ||
| committer | GitHub <noreply@github.com> | |
| Sat, 7 Aug 2021 21:41:46 +0000 (7 23:41 +0200) | ||
| tree | 246a9e32f435781114aa3749d5060b8b5d350580 | treesnapshot (tar.gz zip) |
| parent | bd5e3f4f2e5be52d514af3a5353725cb69bd77eb | commitdiff |
| parent | 91195e844e44f585298c0cb78806103904c4f9bb | commitdiff |
Merge pull request #7510 from Mikolaj/master
Set PATH_SEPARATOR=; when calling ./configure; fix #7494
Set PATH_SEPARATOR=; when calling ./configure; fix #7494