From 9efa102039972ea78f63317caa9da7b91bfd6d72 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 11:37:33 +0200
Subject: Remove unneeded comment

---
 debian/rules | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'debian')

diff --git a/debian/rules b/debian/rules
index 367b34e0..e7d63af6 100755
--- a/debian/rules
+++ b/debian/rules
@@ -59,9 +59,6 @@ ifeq ($(BUILDCACHE),)
 
 	$(MAKE) world STRIP=true
 	$(MAKE) DOC_TARGETS=$(HTMLDOC) $(HTMLDOC)
-	# uncomment to create the cache
-	#mkdir ../coq.cache
-	#rsync -a --exclude=debian --exclude=.git . ../coq.cache/
 else
 	rsync -a --exclude=debian --exclude=.git $(BUILDCACHE)/ .
 endif
-- 
cgit v1.2.3