diff options
| author |  Thomas Capricelli <orzel@freehackers.org> | 2013-03-19 19:18:14 +0100 |
|---|---|---|
| committer | Thomas Capricelli <orzel@freehackers.org> | 2013-03-19 19:18:14 +0100 |
| commit | aba50d842e757d5290c028c9e67e22a3ebd357b4 (patch) | |
| tree | 4ff357d74b761f32bd2e0b83ea74c87176efd000 /scripts | |
| parent | f29b4c435b89b372989db0790e1b28ffa3d2da3a (diff) | |
fixes #568
(files from previous build were kept on the server, with outdated/garbled
information)
The documentation update script now wipes build/doc/html
before rebuilding stuff. Most of the time/cpu consuming is spent in
compiling snippets, so we don't loose that much.
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/eigen_gen_docs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/scripts/eigen_gen_docs b/scripts/eigen_gen_docs index 921d600ed..9b71cd8e0 100644 --- a/scripts/eigen_gen_docs +++ b/scripts/eigen_gen_docs @@ -8,6 +8,7 @@ USER=${USER:-'orzel'} #ulimit -v 1024000 # step 1 : build +rm build/doc/html -Rf mkdir build -p (cd build && cmake .. && make doc) || { echo "make failed"; exit 1; } |