diff options
author | Mauro Bieg <mb21@users.noreply.github.com> | 2018-06-14 18:38:47 +0200 |
---|---|---|
committer | John MacFarlane <jgm@berkeley.edu> | 2018-06-14 09:38:47 -0700 |
commit | 9149155fda27558ac992026edab6ecfc153d7e09 (patch) | |
tree | 08ee6d3a8a9c5b4b81819b195b25bf5160de2337 | |
parent | 48a505c5a07e846c65825994d1be7a403944faf2 (diff) | |
download | pandoc-9149155fda27558ac992026edab6ecfc153d7e09.tar.gz |
MANUAL.txt add proxy description (#4707)
closes #4131
-rw-r--r-- | MANUAL.txt | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/MANUAL.txt b/MANUAL.txt index ae2d4eced..85e93c4fb 100644 --- a/MANUAL.txt +++ b/MANUAL.txt @@ -809,7 +809,8 @@ General writer options : Set the request header *NAME* to the value *VAL* when making HTTP requests (for example, when a URL is given on the command line, or when resources used in a document must be - downloaded). + downloaded). If you're behind a proxy, you also need to set + the environment variable `http_proxy` to `http://...`. Options affecting specific writers ---------------------------------- |