From caa47b9a70389879bbb2009c94ec0071803ff5b2 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Thu, 14 Aug 2014 18:21:19 -0700 Subject: [PATCH] fix(library): add LEAN_VERSION_FILE to Makefile.common --- library/Makefile.common | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/Makefile.common b/library/Makefile.common index 4444b7d75..35a87ef90 100644 --- a/library/Makefile.common +++ b/library/Makefile.common @@ -7,11 +7,11 @@ LEAN_VERSION_FILE = $(shell dirname $(LEAN))/version all: $(OLEAN_FILES) $(DEP_FILES) -%.olean: %.lean +%.olean: %.lean $(LEAN_VERSION_FILE) @rm -f $@ $(LEAN) $(LEAN_OPTIONS) $< -o $@ -c $(@:.olean=.clean) -i $(@:.olean=.ilean) -%.d: %.lean +%.d: %.lean $(LEAN_VERSION_FILE) @echo Making dependency file \'$@\' ... @rm -f $@ @rm -f $@.tmp