On Sun, May 14, 2023, 1:12 PM Tomek CEDRO <to...@cedro.info> wrote: > One last question: how is the website updated? :-P > > By running publish.sh ? > > Is it safe to run? >
This is handled by CI. I just put up a PR to fix the publish issue triggered by your git user.name. Once that merges this will publish. --brennan
