# HG changeset patch
# User wenzelm
# Date 861701832 -7200
# Node ID e5efa177ee0c64770bb182177c2e2454bee3c400
# Parent  8a1eb4531fbb6fb3edbe2476befb64a470d49d0f
removed -norc;

diff -r 8a1eb4531fbb -r e5efa177ee0c bin/isabelle
--- a/bin/isabelle	Tue Apr 22 11:25:45 1997 +0200
+++ b/bin/isabelle	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c bin/isatool
--- a/bin/isatool	Tue Apr 22 11:25:45 1997 +0200
+++ b/bin/isatool	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c build
--- a/build	Tue Apr 22 11:25:45 1997 +0200
+++ b/build	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c configure
--- a/configure	Tue Apr 22 11:25:45 1997 +0200
+++ b/configure	Tue Apr 22 11:37:12 1997 +0200
@@ -6,7 +6,7 @@
 
 ## patch scripts
 
-if bash -norc -c ""
+if bash -c ""
 then
   bash lib/scripts/patch-scripts.bash
 else
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/changeparent
--- a/lib/Tools/changeparent	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/changeparent	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/doc
--- a/lib/Tools/doc	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/doc	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/expandshort
--- a/lib/Tools/expandshort	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/expandshort	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/findlogics
--- a/lib/Tools/findlogics	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/findlogics	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/getenv
--- a/lib/Tools/getenv	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/getenv	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/installfonts
--- a/lib/Tools/installfonts	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/installfonts	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/make
--- a/lib/Tools/make	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/make	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/makeall
--- a/lib/Tools/makeall	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/makeall	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/symbolinput
--- a/lib/Tools/symbolinput	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/symbolinput	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/Tools/usedir
--- a/lib/Tools/usedir	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/Tools/usedir	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/scripts/isa-emacs
--- a/lib/scripts/isa-emacs	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/scripts/isa-emacs	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/scripts/isa-xterm
--- a/lib/scripts/isa-xterm	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/scripts/isa-xterm	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/scripts/run-polyml	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/scripts/run-smlnj	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/scripts/run-smlnj-0.93
--- a/lib/scripts/run-smlnj-0.93	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/scripts/run-smlnj-0.93	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #
diff -r 8a1eb4531fbb -r e5efa177ee0c lib/scripts/ucat
--- a/lib/scripts/ucat	Tue Apr 22 11:25:45 1997 +0200
+++ b/lib/scripts/ucat	Tue Apr 22 11:37:12 1997 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash -norc
+#!/bin/bash
 #
 # $Id$
 #