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

chore(library/Makefile): use C backend

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-24 06:55:52 -07:00
parent 09d8dd536c
commit 6afded1104
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Makefile.in
View file

@ -29,7 +29,7 @@ depends: $(DEPS)
%.olean: %.lean %.depend
@mkdir -p $(STAGE1_DIR)/$(@D)
$(LEAN) $(OPTS) --make --cpp="$(STAGE1_DIR)/$*.cpp.tmp" $<
$(LEAN) $(OPTS) --make --c="$(STAGE1_DIR)/$*.cpp.tmp" $<
# create the .cpp file atomically
mv "$(STAGE1_DIR)/$*.cpp.tmp" "$(STAGE1_DIR)/$*.cpp"
# make sure the .olean file is newer than the .depend file to prevent infinite make cycles