diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-07-04 11:58:21 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:27:32 +0200 |
| commit | 1769cbaddea77112dd6f336316d8eb9a0945a1e6 (patch) | |
| tree | ccd5b36d9d38daa85752c4e677614abc5eeab565 | |
| parent | 17b364613aa7bc04dfdac3efd47e4059afc3ac57 (diff) | |
Keep some file from doc/common/styles/html/simple
They are needed for HTML API doc generation.
| -rwxr-xr-x | debian/purify_tarball | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/debian/purify_tarball b/debian/purify_tarball index a453db06..f1d79961 100755 --- a/debian/purify_tarball +++ b/debian/purify_tarball @@ -1,4 +1,4 @@ -#!/bin/sh +#!/bin/bash set -e @@ -12,7 +12,10 @@ cd $WORKDIR tar zxf $ORIGFILE +mv coq-$VERSION/doc/common/styles/html/simple/{style.css,header.html,footer.html} coq-$VERSION rm -rf coq-$VERSION/doc/common +mkdir -p coq-$VERSION/doc/common/styles/html/simple +mv coq-$VERSION/{style.css,header.html,footer.html} coq-$VERSION/doc/common/styles/html/simple rm -rf coq-$VERSION/doc/faq rm -rf coq-$VERSION/doc/RecTutorial rm -rf coq-$VERSION/doc/refman |