diff options
| author | Emilio Jesus Gallego Arias | 2018-05-17 23:45:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-24 13:21:59 +0200 |
| commit | 5a564f986b5dcb74e347fbdc571d9e1a9980c2a4 (patch) | |
| tree | 0b056da1338cb98e07bfc2271e58054c7ec298d2 /dev/ci | |
| parent | 9392d7ed7c1dfe3ad2b3d6b0f5e039353fbd6517 (diff) | |
[ide] Move common protocol library to its own folder/object.
The `ide` folder contains two different binaries, the language server
`coqidetop` and `coqide` itself.
Even if these binaries are in the same folder, the only thing they
have in common is that they link to the protocol files. In the OCaml
world, having "doubly" linked files in the same project is considered
a bit of an ugly practice, and some build tools such as Dune disallow it.q
Thus, to clean up the build, we move the common protocol files to its
own library `ideprotocol`.
This helps towards Dune integration and towards having an IDE
standalone target, such as the one that was implemented here:
https://github.com/ejgallego/coqide-exp
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/06859-ejgallego-stm+top.sh | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh index ca0076b468..b22ab36302 100644 --- a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh +++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh @@ -1,6 +1,9 @@ #!/bin/sh -if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then +if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || \ + [ "$CI_PULL_REQUEST" = "7543" ] || [ "$CI_BRANCH" = "ide+split" ] ; then + pidetop_CI_BRANCH=stm+top pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git + fi |