summaryrefslogtreecommitdiff
path: root/debian/purify_tarball
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-04 11:58:21 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:27:32 +0200
commit1769cbaddea77112dd6f336316d8eb9a0945a1e6 (patch)
treeccd5b36d9d38daa85752c4e677614abc5eeab565 /debian/purify_tarball
parent17b364613aa7bc04dfdac3efd47e4059afc3ac57 (diff)
Keep some file from doc/common/styles/html/simple
They are needed for HTML API doc generation.
Diffstat (limited to 'debian/purify_tarball')
-rwxr-xr-xdebian/purify_tarball5
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