[haddock @ 2002-04-11 13:40:30 by simonmar]

- copy haddock.css into the same place as the generated HTML

- new option: --css <file>  specifies the style sheet to use

- new option:  -o <dir>  specifies the directory in which to
  generate the output.

- because Haddock now needs to know where to find its default stylesheet,
  we have to have a wrapper script and do the haddock-inplace thing
  (Makefile code copied largely from fptools/happy).

1 files changed, 10 insertions, 0 deletions

diff --git a/src/haddock.sh b/src/haddock.sh
new file mode 100644
index 00000000..b0b534f0
--- /dev/null
+++ b/src/haddock.sh
@@ -0,0 +1,10 @@
+# Mini-driver for Haddock
+
+# needs the following variables:
+#	HADDOCKCSS
+#	HADDOCKBIN
+
+case $* in
+*--css*) $HADDOCKBIN ${1+"$@"};;
+*)       $HADDOCKBIN --css $HADDOCKCSS ${1+"$@"};;
+esac