diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 11:37:33 +0200 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:16:08 +0200 |
| commit | 9efa102039972ea78f63317caa9da7b91bfd6d72 (patch) | |
| tree | 19bf4dcfb14331de42d003114e2950554ba51544 | |
| parent | e347929583f820a2cc0296597b6382309e930989 (diff) | |
Remove unneeded comment
| -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 |