configure
changeset 3007 e5efa177ee0c
parent 2754 59bd96046ad6
child 6029 30c957a74803
     1.1 --- a/configure	Tue Apr 22 11:25:45 1997 +0200
     1.2 +++ b/configure	Tue Apr 22 11:37:12 1997 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  ## patch scripts
     1.6  
     1.7 -if bash -norc -c ""
     1.8 +if bash -c ""
     1.9  then
    1.10    bash lib/scripts/patch-scripts.bash
    1.11  else