aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dev
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dev b/Makefile.dev
index d2a1e9235..db83be369 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -119,7 +119,7 @@ pretyping: pretyping/pretyping.cma
stm: stm/stm.cma
toplevel: toplevel/toplevel.cma
-.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping API
+.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
.PHONY: engine stm toplevel
######################