diff options
Diffstat (limited to 'docs/users_guide')
| -rw-r--r-- | docs/users_guide/flags.xml | 6 | ||||
| -rw-r--r-- | docs/users_guide/ghci.xml | 4 |
2 files changed, 0 insertions, 10 deletions
diff --git a/docs/users_guide/flags.xml b/docs/users_guide/flags.xml index 169dd9d440..53bd4bfb17 100644 --- a/docs/users_guide/flags.xml +++ b/docs/users_guide/flags.xml @@ -493,12 +493,6 @@ <entry>-</entry> </row> <row> - <entry><option>-ghci-script</option></entry> - <entry>Load the given additional <filename>.ghci</filename> file</entry> - <entry>static</entry> - <entry>-</entry> - </row> - <row> <entry><option>-read-dot-ghci</option></entry> <entry>Enable reading of <filename>.ghci</filename> files</entry> <entry>static</entry> diff --git a/docs/users_guide/ghci.xml b/docs/users_guide/ghci.xml index b3fa469a99..3e0d341f83 100644 --- a/docs/users_guide/ghci.xml +++ b/docs/users_guide/ghci.xml @@ -3134,10 +3134,6 @@ warning settings: </varlistentry> </variablelist> - <para>Additional <filename>.ghci</filename> files can be added - through the <option>-ghci-script</option> option. These are - loaded after the normal <filename>.ghci</filename> files.</para> - </sect1> <sect1 id="ghci-obj"> |