Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Some github pages were not rendered properly. This was happening because github will not render files with reserved names. Solution is to add them to the config. A PR is useless because the commit needs to be on the master branch to work. Hence the direct push.
- Loading branch information