From 4db5bdd3562a752017698b70557246404e1d543e Mon Sep 17 00:00:00 2001
From: Mike Pope <mpope@computer.org>
Date: Sat, 17 Oct 2015 07:42:33 +1030
Subject: [PATCH] Include developer manual in release.sh upload.

---
 bin/release.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/bin/release.sh b/bin/release.sh
index fb601f736..41943845b 100755
--- a/bin/release.sh
+++ b/bin/release.sh
@@ -27,12 +27,14 @@ exit
 EOF
 cd ..
 
-if ant manual javadoc ; then
+if ant manual devmanual javadoc ; then
     cd doc
     {
         echo "cd /home/project-web/freecol/htdocs"
         echo "put FreeCol.pdf docs/"
         echo "put FreeCol.html docs/"
+        echo "put developer.pdf docs/"
+        echo "put developer.html docs/"
         echo "put images/* docs/images"
         find javadoc/ -printf "put %p %p\n"
     } | sftp $USERNAME,freecol@web.sf.net