diff options
| author | Pierre-Marie Pédrot | 2019-03-31 23:07:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-31 23:07:48 +0200 |
| commit | 5dd3c18f4e50eef53ae4413b7b80951f17edad5f (patch) | |
| tree | 0a104d6afc109b7b89c8997d1afb3bc9f1e89dc3 /dev | |
| parent | cb502e44aac8328ffd6c37429e050a01f72b2c53 (diff) | |
| parent | f832476404a29d7791c1a6d7970988d3b2e3ad9e (diff) | |
Merge PR #9733: [lexer] keyword protected quotation token for arbitrary text
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/09733-gares-quotations.sh | 6 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 2 |
2 files changed, 7 insertions, 1 deletions
diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh new file mode 100644 index 0000000000..b17454fc4c --- /dev/null +++ b/dev/ci/user-overlays/09733-gares-quotations.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then + + ltac2_CI_REF=quotations + ltac2_CI_GITURL=https://github.com/gares/ltac2 + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index b1bfac8cc9..49251d61a1 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -22,7 +22,7 @@ If you want to build the standard libraries and plugins you should call `make -f Makefile.dune voboot`. It is usually enough to do that once per-session. -More helper targets are availabe in `Makefile.dune`, `make -f +More helper targets are available in `Makefile.dune`, `make -f Makefile.dune` will display some help. Dune places build artifacts in a separate directory `_build`; it will |