From ed44d427cd673fd59004e82e8aed0b6a2d386721 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 7 Nov 2024 22:42:49 -0800 Subject: [PATCH] deploy to pages --- .github/workflows/publish.yml | 52 +++++++++++++++++++++++++++++++++++ playground/tsconfig.json | 4 +-- 2 files changed, 54 insertions(+), 2 deletions(-) create mode 100644 .github/workflows/publish.yml diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml new file mode 100644 index 0000000..1256cf8 --- /dev/null +++ b/.github/workflows/publish.yml @@ -0,0 +1,52 @@ +name: Publish Playground +concurrency: + group: production + cancel-in-progress: true +on: + workflow_dispatch: +jobs: + build: + runs-on: ubuntu-latest + container: ghcr.io/stefan-hoeck/idris2-pack:latest + steps: + - name: checkout + uses: actions/checkout@v2 + + - name: dependencies + uses: actions/setup-node@v4 + with: + node-version: 18 + - name: build + run: | + pack install contrib + make + cd playground + npm install -g esbuild vite + npm install + mkdir public + ./build + vite build --base /newt + #npm run build + - name: Upload playground + id: deployment + uses: actions/upload-pages-artifact@v3 + with: + path: playground/dist/ + deploy: + needs: build + permissions: + pages: write + id-token: write + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + runs-on: ubuntu-latest + steps: + - name: Deploy to GitHub Pages + id: deployment + uses: actions/deploy-pages@v4 + + + + + diff --git a/playground/tsconfig.json b/playground/tsconfig.json index d2c8bf9..a0eb396 100644 --- a/playground/tsconfig.json +++ b/playground/tsconfig.json @@ -20,8 +20,8 @@ /* Linting */ "strict": true, - "noUnusedLocals": true, - "noUnusedParameters": true, + "noUnusedLocals": false, + "noUnusedParameters": false, "noFallthroughCasesInSwitch": true, "noUncheckedSideEffectImports": true },