From 61feac5f33c57dfe31b5b956a0d397ae928fabec Mon Sep 17 00:00:00 2001
From: Chris Hanson <org/chris-hanson/cph>
Date: Sat, 5 Jan 2019 17:46:17 -0800
Subject: [PATCH] Eliminate obsolete comment from user manual.

---
 doc/user-manual/user.texinfo | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/doc/user-manual/user.texinfo b/doc/user-manual/user.texinfo
index 712883ddb..54f90ccb2 100644
--- 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::
-- 
2.25.1