1 files changed, 0 insertions, 10 deletions
diff --git a/configure b/configure
index 9c2618a..13e2181 100755
--- a/configure
+++ b/configure
@@ -17,16 +17,6 @@ bindir='$(PREFIX)/bin'
 libdir='$(PREFIX)/lib/compcert'
 target=''
 
-prompt() {
-    echo "$1 [$x] ? " | tr -d '\n'
-    read y
-    case "$y" in
-        "") ;;
-      none) x="";;
-         *) x="$y";;
-    esac
-}
-
 usage='Usage: ./configure [options] target
 
 Supported targets: