From 8194dc23c0ae03486c22d5e0bf25944142f60d9b Mon Sep 17 00:00:00 2001
From: notin
Date: Mon, 9 Jul 2007 15:59:32 +0000
Subject: Petites corrections sur le Makefile

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9965 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 0aaab2515a..95c26e57d3 100644
--- a/Makefile
+++ b/Makefile
@@ -26,9 +26,9 @@
 
 include config/Makefile
 
-.PHONY: NOARG
+.PHONY: NOARG world worldnodep
 
-NOARG: world
+NOARG: worldnodep
 
 help:
 	@echo "Please use either"
-- 
cgit v1.2.3