Min RK a53178a92b Backport PR #3462: prepare to rename default branch to main ...

- update references to default branch name in docs, workflows
- use HEAD in github urls, which always works regardless of default branch name
- fix petstore URLs since the old petstore links seem to have stopped working

to merge, in order:

- [x] approve this PR
- [x] rename the default branch to main in settings
- [x] merge this PR

Related tangent: I've been using [this git default-branch](https://github.com/minrk/git-stuff/blob/main/bin/git-default-branch) to help with my aliases and friends working with repos with different branch names.

Signed-off-by: Min RK <benjaminrk@gmail.com>

2021-05-12 15:51:06 +02:00

..

source

Backport PR #3462: prepare to rename default branch to main

2021-05-12 15:51:06 +02:00

generate-metrics.py

monitoring docs: fixes following monitoring section relocation

2020-10-01 10:45:11 +02:00

make.bat

Add sphinx skeleton

2016-01-05 19:45:49 -08:00

Makefile

monitoring docs: fixes following monitoring section relocation

2020-10-01 10:45:11 +02:00

package.json

Downgrade bootprint

2020-04-01 14:23:35 +03:00

requirements.txt

Run pre-commit requirements-txt-fixer

2021-02-12 19:24:22 +01:00

rest-api.yml

Backport PR #3462: prepare to rename default branch to main

2021-05-12 15:51:06 +02:00