remove comment

This commit is contained in:
dessant 2015-11-29 23:43:38 +02:00
parent d45af7b8a3
commit d57d533e19
1 changed files with 1 additions and 1 deletions

View File

@ -53,7 +53,7 @@ script:
fi;
- if [ "${RUN}" == "docs" ]; then
make html;
make pdf || true; # first attempt may fail
make pdf || true;
make pdf;
fi;