1 files changed, 0 insertions, 16 deletions
diff --git a/docs/src2texi b/docs/src2texi
deleted file mode 100644
index 10786d9..0000000
--- a/docs/src2texi
+++ /dev/null
@@ -1,16 +0,0 @@
-#! /bin/sh
-#
-# Convert a source file to a TeXinfo file. Stolen from glibc.
-#
-# Usage: src2texi SRCDIR SRC TEXI
-
-dir=$1
-src=`basename $2`
-texi=`basename $3`
-
-sed -e 's,[{}],@&,g'					\
-    -e 's,/\*\(@.*\)\*/,\1,g'				\
-    -e 's,/\*  *,/* @r{,g' -e 's,  *\*/,} */,'		\
-    -e 's/\(@[a-z][a-z]*\)@{\([^}]*\)@}/\1{\2}/g'	\
-    ${dir}/${src} | expand > ${texi}.new
-mv -f ${texi}.new ${dir}/${texi}