From 6ce9ba1ca3f7795cf12798ee1bc6d9d2656f8074 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 10 Apr 2020 18:41:36 -0400
Subject: [ci] [azure] Rework windows Azure pipeline

- use a different mirror for main cygwin archive
- (always) publish build log as artifact
- fix call to dune makefiles
- we do just build Coq for now, as:
  + dune is rebuilding Coq to run the test-suite, this needs move
    investigation.
  + the test suite seems to take long and it times-out on Win.
---
 dev/ci/azure-build.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh
index 04c7d5db91..494651c5bf 100755
--- a/dev/ci/azure-build.sh
+++ b/dev/ci/azure-build.sh
@@ -4,4 +4,4 @@ set -e -x
 
 cd $(dirname $0)/../..
 
-make -f Makefile.dune coq coqide-server
+dune build coq.install coqide-server.install
-- 
cgit v1.2.3