summaryrefslogtreecommitdiff
path: root/.github/workflows
diff options
context:
space:
mode:
authorTom Kelly <ctk21@cl.cam.ac.uk>2021-03-04 16:51:43 +0000
committerTom Kelly <ctk21@cl.cam.ac.uk>2021-03-04 16:51:43 +0000
commitf8460008645c59001c9d1afe4c0327a3fbdad3a4 (patch)
treeef9e96d055eed4ee48a0a7e562733667c9b3bc19 /.github/workflows
parentb9960acd3722b461bb68f56c4e71f03d45bedbec (diff)
downloadocaml-f8460008645c59001c9d1afe4c0327a3fbdad3a4.tar.gz
remove nnp from github workflows
Diffstat (limited to '.github/workflows')
-rw-r--r--.github/workflows/nnp.yml18
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