diff options
Diffstat (limited to 'tools/ghc/ghc-doc-index')
-rwxr-xr-x | tools/ghc/ghc-doc-index | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/tools/ghc/ghc-doc-index b/tools/ghc/ghc-doc-index new file mode 100755 index 0000000..6105d7e --- /dev/null +++ b/tools/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 |