lib/Tools/getenv
changeset 10555 2323ec838401
parent 10511 efb3428c9879
child 14981 e73f8140af78
     1.1 --- a/lib/Tools/getenv	Thu Nov 30 20:07:35 2000 +0100
     1.2 +++ b/lib/Tools/getenv	Thu Nov 30 20:10:29 2000 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -#!/bin/bash
     1.5 +#!/usr/bin/env bash
     1.6  #
     1.7  # $Id$
     1.8  # Author: Markus Wenzel, TU Muenchen