diff options
| author | Sylvain Henry <sylvain@haskus.fr> | 2020-03-02 20:52:59 +0100 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-03-14 05:27:28 -0400 |
| commit | 7432b327a3c43c4e2e7c777b41a8e17899b8d0d1 (patch) | |
| tree | 4b0f3981038def6d5240fa898501d2dfd11adb2b /docs/users_guide | |
| parent | 4f117135673b36816c343bc11efcbb8396160c75 (diff) | |
| download | haskell-7432b327a3c43c4e2e7c777b41a8e17899b8d0d1.tar.gz | |
Use correct option name (-opti) (fix #17314)
s/pgmo/opti
Diffstat (limited to 'docs/users_guide')
| -rw-r--r-- | docs/users_guide/conf.py | 4 | ||||
| -rw-r--r-- | docs/users_guide/ghci.rst | 8 |
2 files changed, 4 insertions, 8 deletions
diff --git a/docs/users_guide/conf.py b/docs/users_guide/conf.py index eb81cf51ec..6fd94db74f 100644 --- a/docs/users_guide/conf.py +++ b/docs/users_guide/conf.py @@ -36,10 +36,6 @@ nitpick_ignore = [ ("c:type", "bool"), - # See #17314 - ("ghc-flag", "-pgmo ⟨port⟩"), - ("ghc-flag", "-pgmo ⟨option⟩"), - ("extension", "DoAndIfThenElse"), ("extension", "RelaxedPolyRec"), diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst index 21102c6846..6fc62544c6 100644 --- a/docs/users_guide/ghci.rst +++ b/docs/users_guide/ghci.rst @@ -3416,10 +3416,10 @@ providing it with a temporary folder (where it will copy the necessary libraries to load to) and port it will listen for the proxy to connect. -Providing :ghc-flag:`-pgmi /path/to/iserv-proxy <-pgmi ⟨cmd⟩>`, -:ghc-flag:`-pgmo ⟨option⟩` and :ghc-flag:`-pgmo ⟨port⟩` in addition to -:ghc-flag:`-fexternal-interpreter` will then make ghc go through the proxy -instead. +Providing :ghc-flag:`-pgmi ⟨/path/to/iserv-proxy⟩ <-pgmi ⟨cmd⟩>` and +:ghc-flag:`-opti ⟨slave-ip⟩ -opti ⟨slave-port⟩ [-opti -v] <-opti ⟨option⟩>` in +addition to :ghc-flag:`-fexternal-interpreter` will then make ghc go through the +proxy instead. There are some limitations when using this. File and process IO will be executed on the target. As such packages like ``git-embed``, |