Remove unused rule from Makefile

sigurdschneider · Sep 20, 2017 · 76b3566 · 76b3566
1 parent 23f210a
commit 76b3566
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/Makefile b/Makefile
@@ -14,6 +14,5 @@ clean:
 $(COQMAKEFILE): Makefile _CoqProject
 	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-%.vo:: $(COQMAKEFILE)
-	make -f $(COQMAKEFILE) -j$(CORES) $@
-
+%:
+	-$(MAKE) -f $(COQMAKEFILE) $@