From 81b2e3a7d41844ec23a57ba15502d2de5cd5b7ac Mon Sep 17 00:00:00 2001 From: RomanNikitenko Date: Tue, 31 Aug 2021 18:25:43 +0300 Subject: [PATCH] chore: Pin che-theia to the upstream Theia commit (#1205) * chore: Pin che-theia to the upstream Theia commit Signed-off-by: Roman Nikitenko --- build.include | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.include b/build.include index 0b1ad841f..2d4d54a4b 100644 --- a/build.include +++ b/build.include @@ -14,7 +14,7 @@ IMAGE_TAG="next" THEIA_GITHUB_REPO="eclipse-theia/theia" THEIA_VERSION="master" THEIA_BRANCH="master" -THEIA_COMMIT_SHA= +THEIA_COMMIT_SHA="9f4f56e388109178dbfed244522bbe49ba474c31" THEIA_GIT_REFS="refs\\/heads\\/master" THEIA_DOCKER_IMAGE_VERSION=