Merging Develop to Main

We wish main and develop to have the same commit hash. This is only possible with git merge --fast-forward. However, GitHub annoyingly doesn't support this through the GUI. Therefore, to merge develop-->main, first open a PR on the GUI, then in command line do:

git fetch
git checkout main
git merge --ff develop
git push

This will automatically close the PR and ensure main and develop are synced.