Copy runtime.txt to publish dir

Author: finsberg

.github/workflows/build_docs.yml

@@ -32,6 +32,7 @@ jobs:
         run: |
           cp -r code ${PUBLISH_DIR}/
           cp -r data ${PUBLISH_DIR}/
+          cp runtime.txt ${PUBLISH_DIR}/
 
       - name: Deploy
         uses: peaceiris/actions-gh-pages@v3