Zsh Mailing List Archive Messages sorted by: Reverse Date, Date, Thread, Author

Re: PATCH: edit-command-line: disable `monitor' option locally

X-seq: zsh-workers 29048
From: Frank Terbeck <ft@xxxxxxxxxxxxxxxxxxx>
To: zsh-workers@xxxxxxx
Subject: Re: PATCH: edit-command-line: disable `monitor' option locally
Date: Tue, 26 Apr 2011 00:25:45 +0200
In-reply-to: <110425092117.ZM1517@torch.brasslantern.com> (Bart Schaefer's message of "Mon, 25 Apr 2011 09:21:17 -0700")
List-help: <mailto:zsh-workers-help@zsh.org>
List-id: Zsh Workers List <zsh-workers.zsh.org>
List-post: <mailto:zsh-workers@zsh.org>
Mailing-list: contact zsh-workers-help@xxxxxxx; run by ezmlm
References: <1300306570-24592-1-git-send-email-ft@bewatermyfriend.org> <110316210401.ZM25580@torch.brasslantern.com> <87tyf2hxe6.fsf@ft.bewatermyfriend.org> <110317082534.ZM26573@torch.brasslantern.com> <87pqppiqbx.fsf@ft.bewatermyfriend.org> <110317181104.ZM26932@torch.brasslantern.com> <874o5mmlcj.fsf@ft.bewatermyfriend.org> <110425092117.ZM1517@torch.brasslantern.com>

Bart Schaefer wrote:
[...]
> the situation with localoptions no_monitor is worse for me than
> without
[...]
> So I reluctantly conclude that you ought to back out the change.

Agreed. [x] done.

Regards, Frank

References:
- PATCH: edit-command-line: disable `monitor' option locally
  - From: Frank Terbeck
- Re: PATCH: edit-command-line: disable `monitor' option locally
  - From: Bart Schaefer
- Re: PATCH: edit-command-line: disable `monitor' option locally
  - From: Frank Terbeck
- Re: PATCH: edit-command-line: disable `monitor' option locally
  - From: Bart Schaefer
- Re: PATCH: edit-command-line: disable `monitor' option locally
  - From: Frank Terbeck
- Re: PATCH: edit-command-line: disable `monitor' option locally
  - From: Bart Schaefer
- Re: PATCH: edit-command-line: disable `monitor' option locally
  - From: Frank Terbeck
- Re: PATCH: edit-command-line: disable `monitor' option locally
  - From: Bart Schaefer

Messages sorted by: Reverse Date, Date, Thread, Author