From 1769cbaddea77112dd6f336316d8eb9a0945a1e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 4 Jul 2009 11:58:21 +0200
Subject: Keep some file from doc/common/styles/html/simple

They are needed for HTML API doc generation.
---
 debian/purify_tarball | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3