top/Makefile: restructured html generation rules
Warning, cannot access the index:
_darcs/index: opening of '_darcs/index' failed: permission denied (Permission denied)
diff -rN -u old-repo/Makefile new-repo/Makefile
--- old-repo/Makefile 2022-09-28 11:17:11.115755556 +0200
+++ new-repo/Makefile 2022-09-28 11:17:11.115755556 +0200
@@ -4,10 +4,6 @@
DIRS = configure src testTop
-ifdef docs
-DIRS += docs
-endif
-
TOPS := $(wildcard *Top)
src_DEPEND_DIRS = configure
@@ -24,10 +20,10 @@
include $(TOP)/configure/RULES_TOP
-docs:
+html:
$(MAKE) -C docs
-upload: docs
+upload: html
rsync -r -t $(TOP)/html/ $(USER_AT_HOST):$(FELLER_PATH)/
darcs push $(DEFAULT_REPO)
darcs push --repo=$(DEFAULT_REPO) -a $(USER_AT_HOST):$(FELLER_PATH)/repo
patch 81746df6b19fd8f44e8c003f6797e3488ee71cc8
Author: benjamin.franksen@helmholtz-berlin.de
Date: Fri Jun 21 14:45:30 CEST 2013
* top/Makefile: restructured html generation rule