1 files changed, 38 insertions, 0 deletions
diff --git a/tools/bootstrap/ghc/ghc-doc-index b/tools/bootstrap/ghc/ghc-doc-index
new file mode 100755
index 0000000..6105d7e
--- /dev/null
+++ b/tools/bootstrap/ghc/ghc-doc-index
@@ -0,0 +1,38 @@
+#!/bin/sh
+
+LOCKFILE=/var/lock/ghc-doc-index.lock
+
+# the lockfile is not meant to be perfect, it's just in case
+# two cron scripts get run close to each other to keep
+# them from stepping on each other's toes.
+if [ -f $LOCKFILE ]; then
+  echo "Locked with $LOCKFILE"
+  exit 0
+fi
+
+if [ "$(id -u)" != "0" ]; then
+  echo Need to be root!
+  exit 1
+fi
+
+trap "{ rm -f $LOCKFILE ; exit 255; }" EXIT
+touch $LOCKFILE
+
+PKGDIRCACHE=/var/lib/ghc/pkg-dir.cache
+LISTING="env LANG=C ls -dl"
+
+# only re-index ghc docs when there are changes
+cd /usr/share/doc/ghc/html/libraries
+if [ -r "$PKGDIRCACHE" ]; then
+  $LISTING */ > $PKGDIRCACHE.new
+  DIR_DIFF=$(diff $PKGDIRCACHE $PKGDIRCACHE.new)
+else
+  $LISTING */ > $PKGDIRCACHE
+fi
+if [ -x "gen_contents_index" -a ! -r "$PKGDIRCACHE.new" -o -n "$DIR_DIFF" ]; then
+  ./gen_contents_index
+fi
+
+if [ -f $PKGDIRCACHE.new ]; then
+  mv -f $PKGDIRCACHE{.new,}
+fi