1 files changed, 0 insertions, 53 deletions
diff --git a/doc/do_docs b/doc/do_docs
deleted file mode 100755
index ef3771a6f4..0000000000
--- a/doc/do_docs
+++ /dev/null
@@ -1,53 +0,0 @@
-#! /bin/sh
-#
-#  $Id$
-#
-
-basedir=$1
-shift
-
-# classes of documents
-supplements="supplements/hppa1_1 supplements/i386 \
-    supplements/i960 supplements/m68k supplements/sparc supplements/powerpc"
-
-# relnotes  is obsolete
-
-# Division by access level
-public_docs="FAQ user develenv networking posix_users itron3.0 \
-    started started_ada rtems_gdb rgdb_specs"
-support_docs="${supplements} bsp_howto filesystem porting ada_user posix1003.1"
-
-if [ x${MANUAL_SET} = x ] ; then
-  MANUAL_SET=public
-fi
-
-case ${MANUAL_SET} in
-  public)
-  #  manuals="$public_docs"
-  #  ;;
-  #support)
-    manuals="$public_docs $support_docs"
-    ;;
-  *)
-    echo "ERROR: Unknown manual set ${MANUAL_SET}"
-    exit 1
-    ;;
-esac
-
-for action in $*
-do
-  for manual in $manuals
-  do
-    if [ x${TEST} = xyes ] ; then
-        echo "TEST *** make $action on ${basedir}/${manual} ***"
-    else
-        echo
-        echo "*** make $action on ${basedir}/${manual} ***"
-        echo
-        cd ${basedir}/${manual}
-        gmake $action || exit $?
-    fi
-  done
-done
-
-exit 0