Skip to content
Snippets Groups Projects
Commit 9ace2001 authored by Michael Sammler's avatar Michael Sammler Committed by Rodolphe Lepigre
Browse files

make ci maybe work

parent 1c22b752
No related branches found
No related tags found
1 merge request!2Dune build
......@@ -18,14 +18,14 @@ variables:
key: "$CI_JOB_NAME"
paths:
- _opam/
only:
- master@iris/refinedc
- /^ci/@iris/refinedc
except:
- triggers
- schedules
- api
- merge_requests
# only:
# - master@iris/refinedc
# - /^ci/@iris/refinedc
# except:
# - triggers
# - schedules
# - api
# - merge_requests
## Build jobs
......
all:
@dune build _build/default/refinedc.install
@dune build _build/default/refinedc.install --display short
.PHONY: all
all_with_examples:
@dune build --display short
.PHONY: all_with_examples
clean:
@dune clean
.PHONY: clean
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment