aboutsummaryrefslogtreecommitdiff
path: root/htmldoc/Makefile
diff options
context:
space:
mode:
authorEnrico Tassi2018-04-20 10:13:36 +0200
committerEnrico Tassi2018-04-20 10:35:01 +0200
commit24a7fea1648991a77fc4ff86a972b0a3935678c8 (patch)
tree4d6043884fafaf062d33c15a266a7f4c92541f79 /htmldoc/Makefile
parent9352fc35ebe04b8b4e9002f3cf39ee1acbab8cd2 (diff)
move the webpage from gh-pages branch to docs/
Diffstat (limited to 'htmldoc/Makefile')
-rw-r--r--htmldoc/Makefile32
1 files changed, 0 insertions, 32 deletions
diff --git a/htmldoc/Makefile b/htmldoc/Makefile
deleted file mode 100644
index d565125..0000000
--- a/htmldoc/Makefile
+++ /dev/null
@@ -1,32 +0,0 @@
-H=@
-
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
-
-SRC=$(shell cd ../mathcomp; ls */*.v | grep -v attic/)
-HEAD=$(shell git symbolic-ref HEAD)
-ifeq "$(HEAD)" "refs/heads/master"
-LAST=$(shell git tag -l --sort=v:refname "mathcomp-*" | tail -n 1)
-RELEASED=$(shell git show $(LAST):mathcomp/Make | grep 'v *$$' | cut -d / -f 2 | cut -d . -f 1)
-endif
-
-all:
- $(H) git diff-index --quiet HEAD ||\
- (echo error: uncommitted files; exit 1)
- $(H) cd ../mathcomp;\
- $(COQBIN)/coqdep -R . mathcomp $(SRC) 2>/dev/null |\
- grep -v vio: > ../htmldoc/depend
- $(H) cat depend | ./buildlibgraph cytoscape $(RELEASED) > depend.js
- $(H) . ../etc/utils/builddoc_lib.sh; \
- cd ../mathcomp; mangle_sources $(SRC)
- $(H) make -C ../mathcomp clean
- $(H) make -C ../mathcomp -j2
- $(H) cd ../mathcomp; $(COQBIN)/coqdoc -t "Mathematical Components"\
- -g --utf8 -R . mathcomp \
- --parse-comments \
- --multi-index $(SRC) -d ../htmldoc/
- $(H) cp ../etc/artwork/coqdoc.css .
- $(H) cd ../mathcomp; git checkout $(SRC)
-
-