# HG changeset patch
# User wenzelm
# Date 1378807073 -7200
# Node ID 05313b45a5aef17abfd53750e879ccf648219d8c
# Parent  07bb77881b8d99e3fb5163cd4a24784e87413b0a
more portable hash-bang;

diff -r 07bb77881b8d -r 05313b45a5ae Admin/MacOS/App1/build
--- a/Admin/MacOS/App1/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/Admin/MacOS/App1/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # Make Isabelle application bundle
 
diff -r 07bb77881b8d -r 05313b45a5ae Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script	Tue Sep 10 11:46:51 2013 +0200
+++ b/Admin/MacOS/App1/script	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # Author: Makarius
 #
diff -r 07bb77881b8d -r 05313b45a5ae Admin/MacOS/App2/mk
--- a/Admin/MacOS/App2/mk	Tue Sep 10 11:46:51 2013 +0200
+++ b/Admin/MacOS/App2/mk	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # Make Isabelle/JVM application bundle
 
diff -r 07bb77881b8d -r 05313b45a5ae Admin/PIDE/convert
--- a/Admin/PIDE/convert	Tue Sep 10 11:46:51 2013 +0200
+++ b/Admin/PIDE/convert	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 THIS="$(cd "$(dirname "$0")"; pwd)"
 SUPER="$(cd "$THIS/.."; pwd)"
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Classes/document/build
--- a/src/Doc/Classes/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Classes/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Codegen/document/build
--- a/src/Doc/Codegen/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Codegen/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Datatypes/document/build
--- a/src/Doc/Datatypes/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Datatypes/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Functions/document/build
--- a/src/Doc/Functions/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Functions/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Intro/document/build
--- a/src/Doc/Intro/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Intro/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/IsarImplementation/document/build
--- a/src/Doc/IsarImplementation/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/IsarImplementation/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/IsarRef/document/build
--- a/src/Doc/IsarRef/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/IsarRef/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/LaTeXsugar/document/build
--- a/src/Doc/LaTeXsugar/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/LaTeXsugar/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Locales/document/build
--- a/src/Doc/Locales/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Locales/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Logics/document/build
--- a/src/Doc/Logics/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Logics/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Main/document/build
--- a/src/Doc/Main/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Main/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Nitpick/document/build
--- a/src/Doc/Nitpick/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Nitpick/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/ProgProve/document/build
--- a/src/Doc/ProgProve/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/ProgProve/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Sledgehammer/document/build
--- a/src/Doc/Sledgehammer/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Sledgehammer/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/System/document/build
--- a/src/Doc/System/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/System/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/Tutorial/document/build
--- a/src/Doc/Tutorial/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/Tutorial/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/ZF/document/build
--- a/src/Doc/ZF/document/build	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/ZF/document/build	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/fixbookmarks
--- a/src/Doc/fixbookmarks	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/fixbookmarks	Tue Sep 10 11:57:53 2013 +0200
@@ -1,3 +1,3 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 perl -pi -e 's/\\([a-zA-Z]+)\s*/$1/g; s/\$//g; s/^BOOKMARK/\\BOOKMARK/g;' "$@"
diff -r 07bb77881b8d -r 05313b45a5ae src/Doc/prepare_document
--- a/src/Doc/prepare_document	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/Doc/prepare_document	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -e
 
diff -r 07bb77881b8d -r 05313b45a5ae src/HOL/IMP/export.sh
--- a/src/HOL/IMP/export.sh	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/HOL/IMP/export.sh	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # Author: Gerwin Klein
 #
diff -r 07bb77881b8d -r 05313b45a5ae src/HOL/TPTP/TPTP_Parser/make_mlyacclib
--- a/src/HOL/TPTP/TPTP_Parser/make_mlyacclib	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/make_mlyacclib	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # make_mlyacclib - Generates Isabelle-friendly version of ML-Yacc's library.
 #
diff -r 07bb77881b8d -r 05313b45a5ae src/HOL/TPTP/TPTP_Parser/make_tptp_parser
--- a/src/HOL/TPTP/TPTP_Parser/make_tptp_parser	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/make_tptp_parser	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # make_tptp_parser - Runs ML-Yacc to generate TPTP parser and makes it
 #                    Isabelle-friendly.
diff -r 07bb77881b8d -r 05313b45a5ae src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py	Tue Sep 10 11:46:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py	Tue Sep 10 11:57:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/usr/bin/python
+#!/usr/bin/env python
 #     Title:      HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
 #     Author:     Daniel Kuehlwein, ICIS, Radboud University Nijmegen
 #     Copyright   2012