Merge branch 'master' onto local working copy

Preserve working copy while updating

1 files changed, 0 insertions, 34 deletions

diff --git a/.github/workflows/web-server.yml b/.github/workflows/web-server.yml
deleted file mode 100644
index 6f14f97b..00000000
--- a/.github/workflows/web-server.yml
+++ /dev/null
@@ -1,34 +0,0 @@
-name: Web server
-
-on:
-    push:
-        paths:
-        - 'web-server/*'
-
-defaults:
-    run:
-        working-directory: web-server
-
-jobs:
-    build:
-        runs-on: ${{ matrix.os }}
-        strategy:
-            matrix:
-                os: [ubuntu-latest]
-                python: [3.8]
-        steps:
-        - uses: actions/checkout@v2
-        - name: Set up Python
-          uses: actions/setup-python@v2
-          with:
-            python-version: ${{ matrix.python }}
-        - name: Install dependencies
-          run: |
-            python -m pip install --upgrade pip
-            pip install -r requirements.txt
-        - name: Lint with pylint
-          run: |
-            ./check.sh
-        - name: Test with pytest
-          run: |
-            pytest opendc