aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Robert Sloan <varomodt@gmail.com>2015-10-22 13:07:57 -0400
committerGravatar Robert Sloan <varomodt@gmail.com>2015-10-22 13:07:57 -0400
commitcf9d1330a883d6ecf5afd43e96b086f4f99bf7e1 (patch)
treeebf7b0d0fe74ea8b76b857370fbf4bbec8501071 /Makefile
parentaa481c0d996c37220fac7d6ab0facb3f7cafe958 (diff)
fix the makefile to not rebuild + module renaming
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 2 insertions, 6 deletions
diff --git a/Makefile b/Makefile
index ecc5dc409..1940c4b2e 100644
--- a/Makefile
+++ b/Makefile
@@ -10,13 +10,9 @@ include .make/coq.mk
FAST_TARGETS += check_fiat check_bedrock clean
.DEFAULT_GOAL = all
-.PHONY: all deps objects clean coquille
+.PHONY: clean coquille
-all: objects
-
-deps: $(SOURCES:%=%.d)
-
-objects: deps $(SOURCES:%=%o)
+all: check_fiat check_bedrock $(SOURCES:%=%o)
clean:
$(RM) $(foreach f,$(SOURCES),$(call coq-generated,$(basename $f)))