From 206ad74aa226d4228a2b7fb263f0c4e3ca2a2ce7 Mon Sep 17 00:00:00 2001 From: rbouckaert Date: Thu, 15 Dec 2022 11:21:22 +1300 Subject: [PATCH] make package manager switch user package dir with -dir option #1070 --- src/beast/pkgmgmt/PackageManager.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/beast/pkgmgmt/PackageManager.java b/src/beast/pkgmgmt/PackageManager.java index b439a105..5c6d829c 100644 --- a/src/beast/pkgmgmt/PackageManager.java +++ b/src/beast/pkgmgmt/PackageManager.java @@ -2043,6 +2043,7 @@ public static void main(String[] args) { if (customDir != null) { String path = PackageManager.getBeastPackagePathProperty(); System.setProperty("BEAST_PACKAGE_PATH", (path != null ? path + ":" : "") +customDir); + System.setProperty("beast.user.package.dir", (path != null ? path + ":" : "") +customDir); } List urlList = getRepositoryURLs();