Closed
Description
There are legacy HTML pages in https://github.com/agda/agda-stdlib/tree/gh-pages which are leftovers from #2147. These pages are still visible (possibly through Google search) like https://agda.github.io/agda-stdlib/Everything.html and https://agda.github.io/agda-stdlib/README.html, etc.
It might be a good idea to suggest the users to visit the new page, e.g. replacing their content by something like
<!DOCTYPE html>
<html>
<head><title>Documentation page moved</title></head>
<body><p>
Documentation has been moved to <a href="https://agda.github.io/agda-stdlib/">https://agda.github.io/agda-stdlib/</a>
</p></body>
</html>