diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-07-15 09:49:40 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-15 09:49:40 +0200 |
| commit | 13e0566dbdd8bf845d7c2a65ffefaaf460381e70 (patch) | |
| tree | 90a8dc86e3bb584ea3218dd3587c85e8efafad54 /Makefile | |
| parent | 72be849e2a9bbe7e8a8438bf561c5a677a35c9e0 (diff) | |
| download | compcert-kvx-13e0566dbdd8bf845d7c2a65ffefaaf460381e70.tar.gz compcert-kvx-13e0566dbdd8bf845d7c2a65ffefaaf460381e70.zip | |
Revised detection of menhirLib directory, continued (#365)
This is a follow-up to commit 3b1f3dd5, which was wrong in that
errors in a shell pipeline were not correctly detected.
Fixes: #363
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions