diff options
-rw-r--r-- | .github/workflows/nnp.yml | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/.github/workflows/nnp.yml b/.github/workflows/nnp.yml deleted file mode 100644 index c5a505dc28..0000000000 --- a/.github/workflows/nnp.yml +++ /dev/null @@ -1,18 +0,0 @@ -name: main - -on: [push, pull_request] - -jobs: - no-naked-pointers: - runs-on: ubuntu-latest - steps: - - name: Checkout - uses: actions/checkout@v2 - - name: configure tree - run: ./configure --disable-naked-pointers --disable-stdlib-manpages - - name: Build - run: | - make -j world.opt - - name: Run the testsuite - run: | - make -C testsuite USE_RUNTIME=d all |