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

chore(library/Makefile): make .olean and .cpp files in a single run

Browse source
This commit is contained in:
Sebastian Ullrich 2019-03-18 19:50:00 +01:00
parent bf5c2ea123
commit 15fe51b8bd
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/Makefile.in
View file

@ -22,18 +22,18 @@ depends: $(DEPS)
@echo $(<:.lean=.olean): `$(LEAN) --deps $< | python relative.py` > $@
%.olean: %.lean %.depend
$(LEAN) $(OPTS) --make $<
@mkdir -p $(STAGE1_DIR)/$(@D)
$(LEAN) $(OPTS) --make --cpp=$(STAGE1_DIR)/$*.cpp $<
# make sure the .olean file is newer than the .depend file to prevent infinite make cycles
@touch $@
@touch $*.olean
clean:
find . -name *.olean -delete
find . -name *.depend -delete
find $(STAGE1_DIR) -name *.cpp -delete
$(STAGE1_DIR)/%.cpp: %.lean %.olean
@mkdir -p $(@D)
$(LEAN) $(OPTS) --cpp=$@ $<
$(STAGE1_DIR)/%.cpp: %.olean
@
$(STAGE1_DIR)/%.o: $(STAGE1_DIR)/%.cpp
../bin/leanc -c -o $@ $< -O3