Closed Finii closed 2 years ago
I'm not sure if we want to use clean
or not. Any opinions?
I'm not sure if we want to use
clean
or not. Any opinions?
Ah, I guess we want to keep clean
. I was wondering about CNAME
, that Lars introduced. I do not really know what that is for, But anyhow, it is preserved, even with clean
:
Ah, I guess we want to keep
clean
. I was wondering aboutCNAME
, that Lars introduced. I do not really know what that is for, But anyhow, it is preserved, even withclean
:
The CNAME is needed for GitHub pages to play nicely with our own domain gul14.info.
Well, looks good to me, but I have little experience with GitHub actions. We might want to discuss if the documentation gets updated with each change in main or only if we tag a release. But IMO "on each push to main" is fine, especially since we annotate each function/class with a "since version X" remark.
We might want to discuss if the documentation gets updated with each change in main or only if we tag a release.
That change would be simple. But at least we have the 'infrastructure' set up now. When it triggers is just a detail ;)
We could also remove to automatic trigger completely and just rely on manually (via web GUI) triggered runs:
That is what workflow_dispatch
is for.
[why] I'm lazy. If there is a change in master, I want up to date documentation.
[how] Let the actions roll...