--- ./lib/Tools/dimacs2hol.orig	Sun Sep  2 15:11:55 2007
+++ ./lib/Tools/dimacs2hol	Sun Sep  2 15:48:05 2007
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
 #
 # $Id: dimacs2hol,v 1.3 2005/04/26 17:50:57 wenzelm Exp $
 # Author: Tjark Weber
@@ -11,7 +11,7 @@
 
 PRG="$(basename "$0")"
 
-function usage()
+usage()
 {
   echo
   echo "Usage: $PRG FILES"