diff options
| author | Emilio Jesus Gallego Arias | 2018-11-14 19:42:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 17:11:51 +0100 |
| commit | c8b6081ebacc0dd8ee1527a271a380dbd3b859b9 (patch) | |
| tree | 622a359d4d1bc57b104ad042a9b1fc5e5d8d11fd /dev/ci | |
| parent | 71938f0de10e1f3b69b1158b80b4898bf3a7dfdb (diff) | |
[vernacextend] Consolidate extension points API
We group the extension API and datatypes under `Vernacextend`.
This means that the base plugin dependency is now `coq.vernac` from
`coq.stm`.
This is quite important as for example the LSP server won't like to
link the STM in.
LTAC still depends on the STM by means of the ltac_profile part tho.
The next step could be to move the extension point below `Vernacexpr`.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh new file mode 100644 index 0000000000..61ffa4a197 --- /dev/null +++ b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then + + ltac2_CI_REF=vernac+move_extend_ast + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + +fi |