--- doc/user/user.tex	2011-12-04 10:41:11.000000000 +0100
+++ doc/user/user.tex	2011-12-04 10:26:44.000000000 +0100
@@ -1,4 +1,5 @@
 % $Id: user.tex,v 1.49 2000-10-14 00:54:07 edo Exp $
+\nonstopmode
 \input{top}
 \usepackage{graphicx}
 \begin{htmlonly}