# 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$ #