diff options
| -rw-r--r-- | docs/users_guide/flags.xml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/docs/users_guide/flags.xml b/docs/users_guide/flags.xml index 5426ad80cf..2f1412796e 100644 --- a/docs/users_guide/flags.xml +++ b/docs/users_guide/flags.xml @@ -493,6 +493,12 @@ <entry>dynamic</entry> <entry>-</entry> </row> + <row> + <entry><option>-fno-print-bind-result</option></entry> + <entry><link linkend="ghci-stmts">Turn off printing of binding results in GHCi</link></entry> + <entry>dynamic</entry> + <entry>-</entry> + </row> </tbody> </tgroup> </informaltable> @@ -1951,12 +1957,6 @@ <entry>dynamic</entry> <entry>-</entry> </row> - <row> - <entry><option>-fno-print-bind-result</option></entry> - <entry><link linkend="ghci-stmts">Turn off printing of binding results in GHCi</link></entry> - <entry>dynamic</entry> - <entry>-</entry> - </row> </tbody> </tgroup> </informaltable> |