Delete the GitHub Wiki - Githubissues

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.

https://wiki.portal.chalmers.se/agda/pmwiki.php

Other

2.46k stars 343 forks source link

Delete the GitHub Wiki #7125

Open lawcho opened 7 months ago

lawcho commented 7 months ago

The GitHub wiki for this repo currently contains only stubs, and has not been touched since Oct 2023.

It should be deleted to:

Avoid fragmentation (we already have the issue tracker, notes in the repo, code comments, user docs, etc.)
Streamline devx (fewer tabs in GitHub)

jespercockx commented 7 months ago

Agreed, I had already forgotten we had activated it.

andreasabel commented 7 months ago

We can use it to have random materials not related to specific issues, like I put a dev meeting protocol there in Oct 2023. Maybe we should put our meeting protocols there more consistently. (I confess I forgot about it.)

lawcho commented 6 months ago

We already have several other stores of "random materials":

The notes/ directory of this repo
The Chalmers Wiki (see also #7126)
Issue tracker comments
- e.g. one of the meeting notes is at https://github.com/agda/agda/issues/3758#issuecomment-1908577638