1 files changed, 0 insertions, 34 deletions
diff --git a/doc/tools/spec-strip-docs b/doc/tools/spec-strip-docs
deleted file mode 100755
index 52d84bc..0000000
--- a/doc/tools/spec-strip-docs
+++ /dev/null
@@ -1,34 +0,0 @@
-#!/bin/sh
-
-DIST_BIN=`dirname "$0"`
-
-CMD=xsltproc
-XSL=${DIST_BIN}/spec-strip-docs.xsl
-
-if test "x$1" = "x" -o  "x$1" = "x-h" -o "x$1" = "x--help"; then
-    echo "usage: $0 [file] ..."
-    exit 1
-fi
-
-if [ ! -r ${XSL} ]; then
-    echo "Cannot find XSLT file"
-    exit 1
-fi
-
-FILES="$@"
-for FILE in $FILES; do
-    echo "${FILE}" | grep ".xml$" > /dev/null
-    if [ $? -ne 0 ]; then
-        echo "Skipping non-xml file: ${FILE}"
-        continue
-    fi
-
-    d=`dirname ${FILE}`
-    b=`basename ${FILE} .xml`
-
-    outfile="${b}-no-docs.xml"
-    echo "Creating: ${outfile}"
-    ${CMD} ${XSL} ${FILE} | tail -n +2  > ${outfile}
-done
-
-exit 0