Configure publishing and update to official 1.20 release

2023-06-07 19:21:30 +02:00
parent 78bec96ae8
commit 9e8eb208f6
5 changed files with 42 additions and 6 deletions
--- a/changelog.md
+++ b/changelog.md
@@ -0,0 +1 @@
+# Dummy file. To be filled by Jenkins