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.