issue !4#1212: filename Clear!.lean contains illegal char...

Stream: triage

[Random Issue Bot]

Today I chose issue 1212 for discussion!

filename Clear!.lean contains illegal character "!"
Created by @Shekhinah Memmel (@herkhinah) on 2022-12-25
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kyle Miller]

There's also Congr!.lean.

I've felt like this file was a sort of test of file name handling for each operating system.

Is Clear!.lean still an issue for Nix users?

[Mario Carneiro]

I assume it is, I don't think anything has changed here since no one uses the nix setup anyway

[Mario Carneiro]

I could see us either renaming the file (easy fix) or making the nix build encode illegal characters since this is a nix restriction, not a lean or OS restriction