# 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