From 8c86262271c209d50461fd352fadf314c2befdd3 Mon Sep 17 00:00:00 2001
From: Phu Tu <phu.tu@hbz-nrw.de>
Date: Mon, 2 Sep 2024 10:46:50 +0200
Subject: [PATCH] Add another FilePermission needed

---
 resources/.java.policy_move_to_home_dir | 1 +
 1 file changed, 1 insertion(+)

diff --git a/resources/.java.policy_move_to_home_dir b/resources/.java.policy_move_to_home_dir
index 9d38004..9bc0b80 100644
--- a/resources/.java.policy_move_to_home_dir
+++ b/resources/.java.policy_move_to_home_dir
@@ -72,6 +72,7 @@ grant {
         permission java.io.FilePermission "${user.home}/git/.project", "read";
         permission java.io.FilePermission "${user.home}/../.project", "read";
         permission java.io.FilePermission "/.project", "read";
+        permission java.io.FilePermission "/opt/.project", "read";
         
         permission java.util.PropertyPermission "*", "read";
         permission java.util.PropertyPermission "jetty.git.hash", "write";