From 5a564f986b5dcb74e347fbdc571d9e1a9980c2a4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 17 May 2018 23:45:26 +0200 Subject: [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 --- dev/ci/user-overlays/06859-ejgallego-stm+top.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh index ca0076b46..b22ab3630 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 -- cgit v1.2.3