generalize a bit; no need to mention my user id directly

diff --git a/Doc/tools/update-docs.sh b/Doc/tools/update-docs.sh
index 3c0a6437abf3cb089829c5512ca00b4a7c4efa38..6599c64d1140ef6f46806511e55b1c0c4252fed3 100755 (executable)
--- a/Doc/tools/update-docs.sh
+++ b/Doc/tools/update-docs.sh
@@ -7,7 +7,7 @@
 # and removes it when done.
 
 if [ -z "$HOME" ] ; then
-    HOME=`grep fdrake /etc/passwd | sed 's|^.*:\([^:]*\):[^:]*$|\1|'`
+    HOME=`grep "$LOGNAME" /etc/passwd | sed 's|^.*:\([^:]*\):[^:]*$|\1|'`
     export HOME
 fi