Skip to content

chore: fix entry for Stone-Weierstrass; remove identifiers#6

Merged
fpvandoorn merged 1 commit into1000-plus:mainfrom
grunweg:MR-fix-entry
Dec 16, 2024
Merged

chore: fix entry for Stone-Weierstrass; remove identifiers#6
fpvandoorn merged 1 commit into1000-plus:mainfrom
grunweg:MR-fix-entry

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Dec 1, 2024

  • the entry for the Stone-Weierstrass theorem was outdated; update the URL
  • remove the 'identifiers' field from this and the continuum hypothesis entry
    (which are the only occurrences of these fields): in fix/chore: update documentation of the file format #7, the identifiers
    fields will be removed from the README.

- the entry for the Stone-Weierstrass theorem was outdated; update the URL
- remove the 'identifiers' field from this and the continuum hypothesis entry
(which are the only occurrences of these fields): in 1000-plus#7, the identifiers
fields will be removed from the README.
@grunweg grunweg changed the title chore: fix entry for Stone-Weierstrass chore: fix entry for Stone-Weierstrass; remove identifiers Dec 16, 2024
@fpvandoorn fpvandoorn merged commit 84cb36e into 1000-plus:main Dec 16, 2024
@grunweg grunweg deleted the MR-fix-entry branch December 16, 2024 12:58
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

Successfully merging this pull request may close these issues.

2 participants