max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(tests/playground/Makefile): create correct .cpp files when called directly

Browse source
This commit is contained in:
Sebastian Ullrich 2019-05-28 11:10:05 +02:00
parent fff2899176
commit 609c27c31f
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/playground/Makefile
View file

@ -50,8 +50,10 @@ frontend%lean.out:
# files of the two binaries.
%.gcc.lean.out: LEAN_BIN = $(LEAN_GCC_BIN)
%.gcc.lean: %.lean; ln -f $< $@
%.no_reuse.lean.cpp: LEAN_BIN = $(LEAN_NO_REUSE_BIN)
%.no_reuse.lean.out: LEAN_BIN = $(LEAN_NO_REUSE_BIN)
%.no_reuse.lean: %.lean; ln -f $< $@
%.no_borrow.lean.cpp: LEAN_BIN = $(LEAN_NO_BORROW_BIN)
%.no_borrow.lean.out: LEAN_BIN = $(LEAN_NO_BORROW_BIN)
%.no_borrow.lean: %.lean; ln -f $< $@
%.no_st.lean.out: LEAN_BIN = $(LEAN_NO_ST_BIN)