Use $LOGNAME instead of $USER to get the current user -- it seems to
be the state of the art.
diff --git a/Doc/Makefile b/Doc/Makefile
index c797b77..b01cbf7 100644
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -51,7 +51,7 @@
 DVIPS=		dvips -f -N0
 MAKEINDEX=	makeindex
 L2H=		latex2html
-L2HARGS=	-address $$USER@`domainname`
+L2HARGS=	-address $$LOGNAME@`domainname`
 
 # Install destination -- not used now but might be useful some time...
 DESTDIR=	/usr/local