--- a/src/Pure/mk	Mon Jul 02 20:55:43 2001 +0200
+++ b/src/Pure/mk	Mon Jul 02 21:02:16 2001 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
changeset 11391	e8638d07fdee
parent 10900	7268a5f425f8
child 14981	e73f8140af78