diff options
-rwxr-xr-x | doc/do_docs | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/doc/do_docs b/doc/do_docs index 2c10189462..db59d824b5 100755 --- a/doc/do_docs +++ b/doc/do_docs @@ -5,9 +5,15 @@ basedir=$1 shift + +# classes of documents +supplements="supplements/hppa1_1 supplements/i386 \ + supplements/i960 supplements/m68k supplements/sparc" +gnu_tools="gnu_tools/newlib-1.8.0 gnu_tools/egcs-1.0.2" + +# Division by access level public_docs="user develenv ka9q posix_users started started_ada" -support_docs="supplements/hppa1_1 supplements/i386 \ - supplements/i960 supplements/m68k supplements/sparc newlib gcc" +support_docs="${supplements} ${gnu_tools} partners_docs="posix1003.1 posix1003.1h" oar_manuals="ada_user hwapi supplements/powerpc tools/texi2www" |