Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

DDOX should always emit case-insensitive file names #228

Open
Geod24 opened this issue Feb 2, 2021 · 0 comments
Open

DDOX should always emit case-insensitive file names #228

Geod24 opened this issue Feb 2, 2021 · 0 comments

Comments

@Geod24
Copy link
Member

Geod24 commented Feb 2, 2021

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 (#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):

struct Pair
{
    Scalar v;
    Point V;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant