diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/eigen_gen_docs | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/scripts/eigen_gen_docs b/scripts/eigen_gen_docs index 3cdacc1a8..17f573673 100644 --- a/scripts/eigen_gen_docs +++ b/scripts/eigen_gen_docs @@ -1,18 +1,17 @@ #!/bin/sh # configuration -USER='orzel' +# You should call this script with USER set as you want, else some default +# will be used +USER=${USER:-'orzel'} -# step 1 : update -hg pull -u || (echo "update failed"; exit 1) - -# step 2 : build +# step 1 : build # todo if 'build is not there, create one: #mkdir build (cd build && cmake .. && make -j3 doc) || (echo "make failed"; exit 1) #todo: n+1 where n = number of cpus -#step 3 : upload +#step 2 : upload BRANCH=`hg branch` if [ $BRANCH == "default" ] then |