# HG changeset patch
# User wenzelm
# Date 950037461 -3600
# Node ID 419157483fc94d2d80ccc08bb25d7c5b8212eb35
# Parent  714f164f038599d4489f35bb770d27a6c52840b9
added -c option (beware!);
changed default DIR to 'document';
NOTE: please ignore last log entry;

diff -r 714f164f0385 -r 419157483fc9 lib/Tools/document
--- a/lib/Tools/document	Tue Feb 08 20:14:58 2000 +0100
+++ b/lib/Tools/document	Tue Feb 08 20:17:41 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash -x
+#!/bin/bash
 #
 # $Id$
 #