data
data copied to clipboard
Katetov's non-normal subspace of $\beta\mathbb{N}$
#360
github is complaining "The head ref may contain hidden characters ...", due to Katetov's name in there. But at least pi-base accepts the name for the preview mode.
FYI for future PRs: (although it may work in this case) In the past we have had cases for example where someone had put a vertical bar in the branch name, and it was impossible to do anything with git, because the vertical bar was interpreted in a special way. It's better to limit the name to ascii characters and some of the non-alphanumeric characters should be avoided.
Someone added S214 so sadly I need to resolve conflicts now...