1 files changed, 0 insertions, 17 deletions
diff --git a/contrib/extraction/test/make_mli b/contrib/extraction/test/make_mli
deleted file mode 100755
index 40ee496e..00000000
--- a/contrib/extraction/test/make_mli
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/usr/bin/awk -We $0
-
-{ match($0,"^open") 
-  if (RLENGTH>0) state=1
-  match($0,"^type") 
-  if (RLENGTH>0) state=1 
-  match($0,"^\(\*\* ")
-  if (RLENGTH>0) state=2
-  match($0,"^let")
-  if (RLENGTH>0) state=0
-  match($0,"^and")
-  if ((RLENGTH>0) && (state==2)) state=0
-  if ((RLENGTH>0) && (state==1)) state=1		     
-  gsub("\(\*\* ","")
-  gsub("\*\*\)","")
-  if (state>0) print
-}