zowoq
|
2a470d0b4e
|
.github/settings.yml: update homepage
|
2023-02-07 08:52:27 +10:00 |
|
Jörg Thalheim
|
b3af80ef38
|
add pogobanane as contributor (#60)
|
2023-02-06 10:21:32 +00:00 |
|
Jörg Thalheim
|
7524c3afd9
|
.github/settings: update repo name
|
2023-02-05 13:20:25 +01:00 |
|
Jörg Thalheim
|
ed7b973d7b
|
Ci (#29)
* allow bors to push
* disable linear history enforcement for bors
|
2023-01-11 23:07:10 +00:00 |
|
Jörg Thalheim
|
0e1de25029
|
allow bors to push (#28)
|
2023-01-11 23:01:58 +00:00 |
|
Jörg Thalheim
|
623ba95ed9
|
undo require bors as required check
This stops bors from merging things... we need a better strategy
here (maybe a check that only runs in staging?)
|
2023-01-11 23:54:17 +01:00 |
|
Lassulus
|
b62a4386af
|
Merge pull request #25 from numtide/repo-settings
add repo settings
|
2023-01-11 18:15:43 +01:00 |
|
zimbatm
|
e982b2d444
|
add repo settings
|
2023-01-11 17:21:35 +01:00 |
|
Jörg Thalheim
|
039bd20578
|
also build github pages in staging
|
2023-01-04 09:41:33 +01:00 |
|
zimbatm
|
932cf2331b
|
CI: publish docs to github pages
|
2022-12-21 19:43:45 +01:00 |
|