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