Eliminate obsolete comment from user manual.

diff --git a/doc/user-manual/user.texinfo b/doc/user-manual/user.texinfo
index 712883ddb10bbb9bac8937bfe3f3b37655f37272..54f90ccb2c37b74078c9faff96c15660f31b7f64 100644 (file)
--- a/doc/user-manual/user.texinfo
+++ b/doc/user-manual/user.texinfo
@@ -1758,9 +1758,6 @@ notification is turned on, turns it off; otherwise turns it on.
 @node Compiling Programs
 @chapter Compiling Programs
 
-Note: the procedures described in this section are only available when
-the @option{--compiler} command-line option is specified.
-
 @menu
 * Compilation Procedures::
 * Declarations::