diff options
| author | Enrico Tassi | 2018-04-12 09:54:36 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-12 09:54:36 +0200 |
| commit | d54b8dff818f0b1218df14cfb2b813da93154fa9 (patch) | |
| tree | b89257dd429d6d57c7efbe6403b9a231392b2a8b /htmldoc/Makefile | |
| parent | c17414bbef21bb3d0b96ee004c29ef7d56e55e2e (diff) | |
remove ssrtest: it now belongs to Coq
Diffstat (limited to 'htmldoc/Makefile')
| -rw-r--r-- | htmldoc/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/htmldoc/Makefile b/htmldoc/Makefile index 5386dca..d565125 100644 --- a/htmldoc/Makefile +++ b/htmldoc/Makefile @@ -4,7 +4,7 @@ ifeq "$(COQBIN)" "" COQBIN=$(dir $(shell which coqtop))/ endif -SRC=$(shell cd ../mathcomp; ls */*.v | grep -v ssrtest/ | grep -v attic/) +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) |