diff --git a/.github/workflows/deploy_docs.yml b/.github/workflows/deploy_docs.yml deleted file mode 100644 index 614144963..000000000 --- a/.github/workflows/deploy_docs.yml +++ /dev/null @@ -1,18 +0,0 @@ -name: Publish docs via GitHub Pages -on: - push: - branches: - - master - -jobs: - build: - name: Deploy docs - runs-on: ubuntu-latest - steps: - - name: Checkout main - uses: actions/checkout@v2 - - - name: Deploy docs - uses: mhausenblas/mkdocs-deploy-gh-pages@master - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.gitignore b/.gitignore deleted file mode 100644 index e87862e4c..000000000 --- a/.gitignore +++ /dev/null @@ -1,5 +0,0 @@ -site/ -*.orig -.ionide/ - -**/.DS_Store \ No newline at end of file diff --git a/.nojekyll b/.nojekyll new file mode 100644 index 000000000..e69de29bb diff --git a/404.html b/404.html new file mode 100644 index 000000000..c5afbf21d --- /dev/null +++ b/404.html @@ -0,0 +1,3809 @@ + + + +
+ + + + + + + + + + + + + + + + + + +{"use strict";/*!
+ * escape-html
+ * Copyright(c) 2012-2013 TJ Holowaychuk
+ * Copyright(c) 2015 Andreas Lubbe
+ * Copyright(c) 2015 Tiancheng "Timothy" Gu
+ * MIT Licensed
+ */var Va=/["'&<>]/;qn.exports=za;function za(e){var t=""+e,r=Va.exec(t);if(!r)return t;var o,n="",i=0,a=0;for(i=r.index;i