|
From: | GNU bug Tracking System |
Subject: | bug#69910: closed ([PATCH] Remove unnecessary group in lua-ts-mode defcustoms) |
Date: | Sat, 23 Mar 2024 07:27:03 +0000 |
Your message dated Sat, 23 Mar 2024 09:25:52 +0200 with message-id <86jzltz9xb.fsf@gnu.org> and subject line Re: bug#69910: [PATCH] Remove unnecessary group in lua-ts-mode defcustoms has caused the debbugs.gnu.org bug report #69910, regarding [PATCH] Remove unnecessary group in lua-ts-mode defcustoms to be marked as done. (If you believe you have received this mail in error, please contact help-debbugs@gnu.org.) -- 69910: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=69910 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems
--- Begin Message ---Subject: [PATCH] Remove unnecessary group in lua-ts-mode defcustoms Date: Tue, 19 Mar 2024 21:03:58 -0500 Tags: patch Another one that got lost. This one drops all the extra ‘:group’s from the defcustoms.
--- End Message ---
--- Begin Message ---Subject: Re: bug#69910: [PATCH] Remove unnecessary group in lua-ts-mode defcustoms Date: Sat, 23 Mar 2024 09:25:52 +0200 > From: john muhl <jm@pub.pink> > Date: Tue, 19 Mar 2024 21:19:16 -0500 > > > john muhl <jm@pub.pink> writes: > > > >> Tags: patch > >> > >> Another one that got lost. This one drops all the extra ‘:group’s > >> from the defcustoms. Thanks, installed on master, and closing the bug.
--- End Message ---
[Prev in Thread] | Current Thread | [Next in Thread] |