My local git instance keeps showing that I have an unstaged change to the file doc/actec/zerodim2pol_0_0.md.
Was a little puzzled by this until I realized there are actually two versions of this file in the repo:
doc/actec/zerodim2pol_0_0.md (lowercase z)
doc/actec/Zerodim2pol_0_0.md (uppercase Z)
These both seem to have been introduced via a methodical database update by @cdjackson, so not sure if just submitting a PR to delete one of these files would be sufficient. The files are not quite exact duplicates of each other but I assume one is unintentional.
Obviously I could work around by doing development on a case sensitive filesystem, but may be worth fixing to avoid creating confusion for future contributors.
My local git instance keeps showing that I have an unstaged change to the file
doc/actec/zerodim2pol_0_0.md.Was a little puzzled by this until I realized there are actually two versions of this file in the repo:
doc/actec/zerodim2pol_0_0.md(lowercasez)doc/actec/Zerodim2pol_0_0.md(uppercaseZ)These both seem to have been introduced via a methodical database update by @cdjackson, so not sure if just submitting a PR to delete one of these files would be sufficient. The files are not quite exact duplicates of each other but I assume one is unintentional.
Obviously I could work around by doing development on a case sensitive filesystem, but may be worth fixing to avoid creating confusion for future contributors.