Mini bugfix.

diff --git a/docs/api/make_pdf_manuals.sh b/docs/api/make_pdf_manuals.sh
index a4af45ad22db7ae4bbad6084954ff0a225fb6814..9b67e41c22d12ad12ca4aec3be4733742e6c6f54 100755 (executable)
--- a/docs/api/make_pdf_manuals.sh
+++ b/docs/api/make_pdf_manuals.sh
@@ -4,9 +4,9 @@
 #
 # $Id#
 
-#if [ -d admin ]; then
-#      cp -a devel admin
-#fi
+if [ ! -d admin ]; then
+       cp -a devel admin
+fi
 
 cat admin/main.tex | sed 's/{\\rm.\{5,50\}})}//g' > admin/main2.tex
 mv -f admin/main2.tex admin/main.tex