| commit | b5c29644d7ee2589f859be11b10659115ec46085 | |
| author | Mikolaj Konarski <mikolaj@well-typed.com> | |
| Wed, 15 Sep 2021 10:46:32 +0000 (15 12:46 +0200) | ||
| committer | GitHub <noreply@github.com> | |
| Wed, 15 Sep 2021 10:46:32 +0000 (15 12:46 +0200) | ||
| tree | b5b694a6981673768a5e326815fc6f708ec79147 | treesnapshot (tar.gz zip) |
| parent | d9ec979a2fe0c6ef50778724acd218154034fe4c | commitdiff |
| parent | 37ccc45cb7cd6008d69a22b58138deb167edab26 | commitdiff |
Merge pull request #7651 from Mikolaj/master
Revert PR #7510 (which was "Set PATH_SEPARATOR=; when calling ./configure")
Revert PR #7510 (which was "Set PATH_SEPARATOR=; when calling ./configure")