Stream: rustdoc

Topic: case insensitive fix


view this post on Zulip GuillaumeGomez (Mar 26 2021 at 12:05):

I just thought about a solution that might fix the name conflicts and wouldn't require to change the URL pattern we're using:

We could check for all the items we'll generate and when there is a conflict, still generate a file which would contain the headers and only a <script> tag which would load the correct file based on the URL in the current HTML directly.

What do you think?

view this post on Zulip Joshua Nelson (Mar 26 2021 at 13:32):

Hmm I don't think that would actually help - the redirect file could overwrite the one with different casing or vice versa

view this post on Zulip GuillaumeGomez (Mar 26 2021 at 18:33):

no I mean, before starting generating files, we check if some would conflict in case insensitive scenario. For those conflicts, we generate a html file which contains a <script> which will load the correct html depending on the URL

view this post on Zulip GuillaumeGomez (Mar 26 2021 at 18:33):

Is it more clear?

view this post on Zulip Joshua Nelson (Mar 26 2021 at 18:45):

oh I see! I like that :)

view this post on Zulip Joshua Nelson (Mar 26 2021 at 18:46):

I think all the case-insensitive files are still case-preserving, you'd need to test it though

view this post on Zulip GuillaumeGomez (Mar 26 2021 at 19:15):

At least on windows, it opens the same file, whatever the case. So we should be fine.

view this post on Zulip Noah Lev (Mar 26 2021 at 23:05):

This seems like a neat idea, but I wonder if there are some browsers that have case-insensitive URLs? Maybe we don't worry about that, but I thought it's worth bringing up just in case.

Also, I'd rather avoid using more JS. But I guess this seems like the best solution so far :)


Last updated: Oct 11 2021 at 22:34 UTC