create subdirs man1 and man7 on the web

Signed-off-by: Nico Schottelius <nico@kr.ethz.ch>

build.sh

@@ -96,10 +96,14 @@ case "$1" in
       
    web)
       cp README ${WEBDIR}/${WEBPAGE}
-      rm -rf ${WEBDIR}/${WEBBASE}/man && mkdir ${WEBDIR}/${WEBBASE}/man
+      rm -rf ${WEBDIR}/${WEBBASE}/man 
+      mkdir ${WEBDIR}/${WEBBASE}/man/man1
+      mkdir ${WEBDIR}/${WEBBASE}/man/man7
+
       rm -rf ${WEBDIR}/${WEBBASE}/speeches && mkdir ${WEBDIR}/${WEBBASE}/speeches
 
-      cp ${MAN1DSTDIR}/*.html ${MAN7DSTDIR}/*.html ${WEBDIR}/${WEBBASE}/man
+      cp ${MAN1DSTDIR}/*.html ${WEBDIR}/${WEBBASE}/man/man1
+      cp ${MAN7DSTDIR}/*.html ${WEBDIR}/${WEBBASE}/man/man7
       cp ${SPEECHESDIR}/*.pdf ${WEBDIR}/${WEBBASE}/speeches
       
       git describe > ${WEBDIR}/${WEBBASE}/man/VERSION