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 8569da67edad9759c0b6b9b07e6885e714bfeb55..b69f448193af0da227f5312023a9dbc4c0a957a6 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