diff options
Diffstat (limited to 'test_smiri.sh')
| -rwxr-xr-x | test_smiri.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test_smiri.sh b/test_smiri.sh index 0dbad3fa..a275420a 100755 --- a/test_smiri.sh +++ b/test_smiri.sh @@ -2,6 +2,7 @@ set -e cd $(dirname $0) make -f minicargo.mk MMIR=1 LIBS +make -C tools/standalone_miri echo "--- mrustc -o output-mmir/hello" ./bin/mrustc rustc-1.19.0-src/src/test/run-pass/hello.rs -O -C codegen-type=monomir -o output-mmir/hello -L output-mmir/ > output-mmir/hello_dbg.txt echo "--- standalone_miri output-mmir/hello.mir" |