From 24bdc17dfd94b99ff5aa216fc6ed073b42146b37 Mon Sep 17 00:00:00 2001
From: Bastian Kleineidam <calvin@debian.org>
Date: Wed, 6 Apr 2011 18:54:19 +0200
Subject: [PATCH] Note that configuration changes require a GUI restart.

---
 doc/html/options.html | 4 +++-
 doc/html/options.txt  | 3 ++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/doc/html/options.html b/doc/html/options.html
index 61bf13bb..b3ccd75a 100644
--- a/doc/html/options.html
+++ b/doc/html/options.html
@@ -45,7 +45,9 @@ It can be displayed with Help->Show Debug</p>
 
 <h2>Configuration files</h2>
 
-<p>The configuration files can be edited with an integrated text editor.</p>
+<p>The configuration files can be edited with an integrated text editor.
+Note that changes to the configuration files require a restart of
+the GUI to take effect.</p>
 <hr/>
     <div class="footer">
       &copy; Copyright 2011, Bastian Kleineidam.
diff --git a/doc/html/options.txt b/doc/html/options.txt
index 5cd03431..5774965b 100644
--- a/doc/html/options.txt
+++ b/doc/html/options.txt
@@ -17,4 +17,5 @@ It can be displayed with Help->Show Debug
 
 ## Configuration files
 The configuration files can be edited with an integrated text editor.
-
+Note that changes to the configuration files require a restart of
+the GUI to take effect.