fix(docker): Pre-create "$HOME/.gradle" for proper permissions #9935
Conversation
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## main #9935 +/- ##
=========================================
Coverage 68.46% 68.46%
Complexity 1309 1309
=========================================
Files 250 250
Lines 8881 8881
Branches 924 924
=========================================
Hits 6080 6080
Misses 2409 2409
Partials 392 392
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Sentry. |
Dockerfile
Outdated
| @@ -582,8 +582,8 @@ ENV PATH=$PATH:/opt/ort/bin | |||
| USER $USER | |||
| WORKDIR $HOME | |||
|
|
|||
| # Ensure that the ORT data directory exists to be able to mount the config into it with correct permissions. | |||
| RUN mkdir -p "$HOME/.ort" | |||
| # Ensure that data directories exist to be able to mount volumes from the host into them with correct permissions. | |||
There was a problem hiding this comment.
Nit: Maybe just "that these directories" and scratch "into them" (same below).
There was a problem hiding this comment.
I somehow wanted to express that this mostly is about existing data on the host being made available in the container, and that there is only a problem if you mount "into" a nested path inside the container where any intermediate path is not existing in the container.
There was a problem hiding this comment.
I found that it sounds weird but it's just a nit anyway.
Fixes #9756. Signed-off-by: Sebastian Schuberth <[email protected]>
sschuberth
force-pushed
the
docker-gradle-home
branch
from
60b7627 to
3022127
Compare
|
Merging despite the unrelated |
Fixes #9756.