[ jedit-Patches-3522179 ] replacing Global Options with Options

Patches item #3522179, was opened at 2012-04-27 23:44
Message generated for change (Comment added) made by ezust
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=300588&aid=3522179&group_id=588

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: docs
Group: None
>Status: Closed
>Resolution: Accepted
Priority: 5
Private: No
Submitted By: Jarek Czekalski (jarekczek)
Assigned to: Alan Ezust (ezust)
Summary: replacing Global Options with Options

Initial Comment:
I thought it would be a quick stab, but it turned into a long task. Finally I think I managed to replace all the
references to Global Options menu item, which no longer exists. In most cases it's just changed to
Options. Only in customizing.xml I did write something:

-        <para><guimenu>Utilities</guimenu>&gt;<guimenuitem>Global
-        Options</guimenuitem> displays the global options dialog box. The dialog
+        <para><guimenu>Utilities</guimenu>&gt;<guimenuitem>Options</guimenuitem>
+        displays the options dialog box.
+        It has 2 tabs, the first one is <guimenu>Global Options</guimenu>.
+        The dialog