Some systems are not case-sensitive, and having DDOX emit case-sensitive names means documentation might break on those systems. One example I came across is when uploading documentation to github pages using actions/upload-artifacts:
Uploads are case insensitive: /home/runner/work/agora/agora/docs/agora/common/crypto/Schnorr/Pair.v.html was detected that it will be overwritten by another file with the same path
There was a warning added on Windows and OSX (https://github.com/rejectedsoftware/ddox/issues/84) but this is a build performed on Ubuntu, which uploads to a case-insensitive file-system. I think DDOX should just emit case-insensitive file names instead of requiring the user to use --file-name-style=lowerUnderscored.
Some systems are not case-sensitive, and having DDOX emit case-sensitive names means documentation might break on those systems. One example I came across is when uploading documentation to github pages using
actions/upload-artifacts
:There was a warning added on Windows and OSX (https://github.com/rejectedsoftware/ddox/issues/84) but this is a build performed on Ubuntu, which uploads to a case-insensitive file-system. I think DDOX should just emit case-insensitive file names instead of requiring the user to use
--file-name-style=lowerUnderscored
.In our case, the issues is (simplified):