You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: INSTALL.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -112,5 +112,5 @@ The aggregated results of the validation can be found in the following files.
112
112
### No results after validation, or 'cannot create directory '../results/difftrees': Permission denied'
113
113
`Problem:` This problem can occur due to how permissions are managed inside the Docker container. More specifically, it will appear, if Docker is executed with elevated permissions (i.e., `sudo`) and if there is no [results](results) directory because it was deleted manually. In this case, Docker will create the directory with elevated permissions, and the Docker user has no permissions to access the directory.
114
114
115
-
`Fix:` If there is a _results_ directory delete it (e.g., via your file explorer).
115
+
`Fix:` If there is a _results_ directory delete it with elevated permission (e.g., `sudo rm -r results`).
116
116
Then, create a new _results_ directory without elevated permissions, or execute `git restore .` to restore the deleted directory.
0 commit comments