Skip to content
Snippets Groups Projects
Commit 26cd1373 authored by Giovanni Bussi's avatar Giovanni Bussi
Browse files

Smaller manual on travis-ci 

Copy only necessary files

[makedoc]
parent 0c5ca1fc
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 5 additions and 4 deletions
.travis.pushdoc
+ 5
− 4
View file @ 26cd1373
...@@ -10,10 +10,11 @@ mkdir -p tmp/$$ ...@@ -10,10 +10,11 @@ mkdir -p tmp/$$
cd tmp/$$ cd tmp/$$
# grab doc # grab doc
cp -R $root/*doc . mkdir user-doc
cp -R $root/user-doc/{*.png,html,manual.pdf} user-doc/
# delete gitignore files test -d $root/user-doc/regtests && cp -R $root/user-doc/regtests user-doc/ || true
rm */.gitignore mkdir developer-doc
cp -R $root/developer-doc/{*.png,html} developer-doc/
# This file should be here, it is needed otherwise # This file should be here, it is needed otherwise
# files beginning with _ are skipped # files beginning with _ are skipped
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment