diff options
| author | Léonard Oest O'Leary <lool4516@gmail.com> | 2023-05-23 13:55:06 -0400 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-05-23 13:55:06 -0400 |
| commit | 9db4b5c533fe65ad7449757d5afecf8e0853dc9e (patch) | |
| tree | 13d0caf5579e727adcc2bc10f4fa4ea3f8a50240 | |
| parent | 13090a80b0db51f0fdecc4c4322bdd3eb2f1e9c3 (diff) | |
| parent | 5e6bdf4d4e40df6ae647d15983a2d6055845beb4 (diff) | |
Merge pull request #19 from leo-ard/idris2-host
fix make check on idris2 host
| -rw-r--r-- | src/host/idr/makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/host/idr/makefile b/src/host/idr/makefile index b703e7a..a129c83 100644 --- a/src/host/idr/makefile +++ b/src/host/idr/makefile @@ -6,9 +6,10 @@ check: options=`sed -n -e '/;;;options:/p' $$prog | sed -e 's/^;;;options://'`; \ echo "---------------------- $$prog [options:$$options]"; \ rm -rf test.idr*; \ - gsi ../../rsc.scm -t idr $$options -o test.idr $$prog; \ + ../../rsc -t idr $$options -o test.idr $$prog; \ idris2 -o test.idr.exe --output-dir . test.idr; \ sed -n -e '/;;;input:/p' $$prog | sed -e 's/^;;;input://' | ./test.idr.exe > test.idr.out; \ + sleep 1 `# For some reason, idris2 takes time to write to file`; \ sed -e '1,/;;;expected:/d' -e 's/^;;;//' $$prog | diff - test.idr.out; \ done |