@end example
@end quotation
-Close the file and save it. Run the following command a few times (at
-least three times) until it says @code{PS output to `foo.ps', DVI output
-to `foo.dvi'}.
+Close the file and save it. Run the following command. It should say
+@code{PS output to `foo.ps', DVI output to `foo.dvi'}.
@quotation
@example