From a0289dd49f8111f743aa3b8858fb89d24bcf015b Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Wed, 7 Oct 2020 18:07:08 -0500 Subject: [PATCH] Fix updated repo name in Jenkins integration --- Jenkinsfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Jenkinsfile b/Jenkinsfile index 3a50777ec..9d4c5deaa 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -95,7 +95,7 @@ melt.trynode('silver') { stage("Integration") { // Projects with 'develop' as main branch, we'll try to build specific branch names if they exist def github_projects = ["/melt-umn/ableC", "/melt-umn/Oberon0", "/melt-umn/ableJ14", "/melt-umn/meta-ocaml-lite", - "/melt-umn/rewriting-lambda-calculus", "/melt-umn/rewriting-regex-matching", "/melt-umn/rewriting-optimization-demo", + "/melt-umn/lambda-calculus", "/melt-umn/rewriting-regex-matching", "/melt-umn/rewriting-optimization-demo", "/internal/ring"] // Specific other jobs to build def specific_jobs = ["/internal/matlab/master", "/internal/metaII/master", "/internal/simple/master"]