diff options
Diffstat (limited to 'docs/users_guide/ghci.rst')
| -rw-r--r-- | docs/users_guide/ghci.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst index 78c74c5dc3..6ff9c1f20a 100644 --- a/docs/users_guide/ghci.rst +++ b/docs/users_guide/ghci.rst @@ -3303,6 +3303,7 @@ read: .. ghc-flag:: -ignore-dot-ghci :shortdesc: Disable reading of ``.ghci`` files :type: dynamic + :reverse: -no-ignore-dot-ghci :category: Don't read either :file:`./.ghci` or the other startup files when |