diff options
| -rwxr-xr-x | debian/rules | 3 |
1 files changed, 0 insertions, 3 deletions
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 |