Robbert van der Helm
|
16ba6cffdc
|
Deploy the docs to a different repo
To avoid adding polluting the GitHub feed with a ton of noise when
watching this one.
|
2022-04-26 20:20:14 +02:00 |
|
|
Robbert van der Helm
|
fc4386a585
|
Fix refresh page HTML
|
2022-04-11 17:11:52 +02:00 |
|
|
Robbert van der Helm
|
f9ccb40fc4
|
Fix path in docs workflow
|
2022-04-11 16:59:07 +02:00 |
|
|
Robbert van der Helm
|
caadc06947
|
Rename docs workflow
|
2022-04-11 16:56:49 +02:00 |
|
|
Robbert van der Helm
|
755780f2a9
|
Generate docs on GitHub pages
|
2022-04-11 16:55:10 +02:00 |
|