On Sat, Oct 14, 2023 at 9:15 PM Joseph Kesselman <kesh...@alum.mit.edu> wrote:
> Taking out the META-INF: I'll look at that. ... quibbles like editor > configurations and unnecessary files can be cleaned up in subsequent edits; > they shouldn't be considered blockers now. > Sure. Just an opportunity to remove files and thereby reduce the size of the changeset. They may mostly be relocations, but GitHub's UI still struggles under the weight of 1400 changes in a single PR.
