diff options
-rw-r--r-- | debian/gbp.conf | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/debian/gbp.conf b/debian/gbp.conf index 92f87323..e7255ba1 100644 --- a/debian/gbp.conf +++ b/debian/gbp.conf @@ -17,12 +17,9 @@ filter = [ "doc/common/styles/html/coqremote/styles.hva", "doc/common/styles/html/simple/cover.html", "doc/common/styles/html/simple/hevea.css", - "doc/common/styles/html/simple/modules", - "doc/common/styles/html/simple/sites", "doc/common/styles/html/simple/styles.hva", "doc/common/macros.tex", "doc/common/title.tex", - "doc/refman", "doc/sphinx", "doc/tools/coqrst/regen_readme.py", "doc/tools/latex_filter", @@ -37,13 +34,6 @@ filter = [ "tactics/doc.tex", "vernac/doc.tex", - # The Coq Tutorial, licensed under the non-free Open Publication License. - "doc/tutorial", - - # The Tutorial on [Co-]Inductive Types, licensed under the non-free Open - # Publication License. - "doc/RecTutorial", - # Fonts licensed under the non-free Ubuntu Font Licence. "doc/tools/coqrst/notations/CoqNotations.ttf", "doc/tools/coqrst/notations/UbuntuMono-B.ttf", |