diff options
| -rw-r--r-- | doc/misc/idlwave.texi | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/misc/idlwave.texi b/doc/misc/idlwave.texi index f6d702c4963..496674cd64b 100644 --- a/doc/misc/idlwave.texi +++ b/doc/misc/idlwave.texi | |||
| @@ -3817,7 +3817,7 @@ equivalents (yet can be bookmarked, browsed as history, searched, | |||
| 3817 | etc.). | 3817 | etc.). |
| 3818 | 3818 | ||
| 3819 | @c Not updated in over a decade. | 3819 | @c Not updated in over a decade. |
| 3820 | @C Maybe you want to recommend eww these days. | 3820 | @c Maybe you want to recommend eww these days. |
| 3821 | @ignore | 3821 | @ignore |
| 3822 | @noindent Individual platform recommendations: | 3822 | @noindent Individual platform recommendations: |
| 3823 | 3823 | ||