add github links and publish script

2023-03-28 22:19:55 +02:00
parent 6a1a184e2f
commit b78a8d061c
2 changed files with 5 additions and 0 deletions
@@ -0,0 +1,3 @@
+git add dist -f
+git commit -m 'publish'
+git subtree push --prefix dist origin gh-pages