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

chore: ignore stale .c file at update-stage0

Browse source
This commit is contained in:
Sebastian Ullrich 2019-12-11 17:13:55 +01:00 • committed by Leonardo de Moura
parent 0c9f01ac18
commit 203bf76ff4
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Makefile.in
View file

@ -55,7 +55,7 @@ $(OUT)/libleanstdlib.a: $(addprefix $(OUT)/,$(SRCS:.lean=.o))
update-stage0:
-rm -r $(STAGE0_DIR)
-mkdir -p $(STAGE0_DIR)/stdlib
cp -R $(C_OUT) $(STAGE0_DIR)/stdlib/Init
for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/Init/$$f`; cp $(C_OUT)/$$f $(STAGE0_DIR)/stdlib/Init/$$f; done
echo "add_library (stage0 OBJECT $(CS_CORE))" > $(STAGE0_DIR)/stdlib/CMakeLists.txt
# don't copy untracked crap
cd ..; git ls-files -z . | xargs -0 -I '{}' bash -c 'mkdir -p `dirname ../stage0/src/{}` && cp {} ../stage0/src/{}'