# HG changeset patch # User wenzelm # Date 913912892 -3600 # Node ID 30c957a7480329b5c694bb4169d96ee801f22fb0 # Parent 1bfd52528bdeb77e8d4b8ce338373fe178ed8f83 bash -c :; diff -r 1bfd52528bde -r 30c957a74803 configure --- a/configure Fri Dec 11 18:57:00 1998 +0100 +++ b/configure Thu Dec 17 17:41:32 1998 +0100 @@ -6,7 +6,7 @@ ## patch scripts -if bash -c "" +if bash -c : then bash lib/scripts/patch-scripts.bash else