use provided $USER if available, let the caller do the update (safer)

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