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 3c0a643..6599c64 100755
--- 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