From 9149155fda27558ac992026edab6ecfc153d7e09 Mon Sep 17 00:00:00 2001
From: Mauro Bieg <mb21@users.noreply.github.com>
Date: Thu, 14 Jun 2018 18:38:47 +0200
Subject: [PATCH] MANUAL.txt add proxy description (#4707)

closes #4131
---
 MANUAL.txt | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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
 ----------------------------------