# HG changeset patch
# User wenzelm
# Date 994100536 -7200
# Node ID e8638d07fdee6d37a9dd328782dcf9a9bf5323a7
# Parent  735bf767833adc727c8dde7a8feb6115b380e2e0
#!/usr/bin/env bash;

diff -r 735bf767833a -r e8638d07fdee src/Pure/mk
--- 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