fix makeofflinedoc.sh image downloading

- check Tutorial.html because there is an index.html in other
directories
- also download .svg files

diff --git a/contrib/utilities/makeofflinedoc.sh b/contrib/utilities/makeofflinedoc.sh
index 229a109709685f6a6f04c48f2c8c9fce077a2e99..9a5b29913fe73f6fd19e667835fda747d5881537 100755 (executable)
--- a/contrib/utilities/makeofflinedoc.sh
+++ b/contrib/utilities/makeofflinedoc.sh
@@ -18,9 +18,9 @@
 # the URLs to point to the local files. To be run in the doc/doxygen/deal.II
 # directory of an installed deal.II documentation.
 
-if [ ! -f index.html ]
+if [ ! -f Tutorial.html ]
 then
-  echo "Please run this script in the doc output directory (install/doc)"
+  echo "Please run this script in the doc output directory (<install>/doc/doxygen/deal.II)"
   exit 1
 fi
 
@@ -30,7 +30,7 @@ echo "Downloading images (press ctrl-c to cancel) ..."
 cd images
 {
 trap "echo \"(skipping)\"" SIGINT
-wget -q -nd -A png,gif -m -l 1 -np http://www.dealii.org/images/steps/developer/
+wget -q -nd -A svg,png,gif -m -l 1 -np http://www.dealii.org/images/steps/developer/
 }
 rm robots.txt*
 cd ..