# 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