Closed rgrunber closed 2 weeks ago
Is it also worth updating in the gulpfile? i.e.
diff --git a/gulpfile.js b/gulpfile.js
index b0ca41a..1bdd4ca 100644
--- a/gulpfile.js
+++ b/gulpfile.js
@@ -282,7 +282,7 @@ function download_server_fn(){
function build_server_fn(){
fse.removeSync('./server');
- cp.execSync(mvnw() + ' -Pserver-distro clean package -Declipse.jdt.ls.skipGradleChecksums', { cwd: server_dir, stdio: [0, 1, 2] });
+ cp.execSync(mvnw() + ' -Pserver-distro clean package -Declipse.jdt.ls.skipGradleChecksums -U ', { cwd: server_dir, stdio: [0, 1, 2] });
gulp.src(server_dir + '/org.eclipse.jdt.ls.product/distro/*.tar.gz', { encoding: false })
.pipe(decompress())
.pipe(gulp.dest('./server'));
(I was using this locally)