configure
changeset 103 de27336a2273
parent 102 ae97422b2857
child 104 0d3b8c9b24d2
--- a/configure	Tue May 03 16:41:41 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-#! /bin/bash
-
-prefix="/usr/local"
-
-tmp=$(getopt -n $0 -o p -l prefix: -- "$@")
-eval set -- "$tmp"
-
-while true; do
-    case "$1" in 
-	--prefix)   prefix="$2"; shift 2
-		    ;;
-	--)	    break
-		    ;;
-    esac
-done
-
-
-set -e
-umask 0333
-sed -e "s|@prefix@|$prefix|g" <Makefile.in >Makefile.$$
-rm -f Makefile
-mv Makefile.$$ Makefile