diff options
| author | Thomas Wolf <thomas.wolf@paranor.ch> | 2018-08-19 20:48:06 +0200 |
|---|---|---|
| committer | David Pursehouse <david.pursehouse@gmail.com> | 2018-09-11 08:26:52 +0900 |
| commit | 94fad4412ae151c0a71150e8b83edc0ecd10adf3 (patch) | |
| tree | f267152d76a01f5206dc9e710816af9b00117db6 /org.eclipse.jgit.pgm/build.properties | |
| parent | 6fe4505b2a753173ff9708c2c71cb833aaacf016 (diff) | |
| download | jgit-94fad4412ae151c0a71150e8b83edc0ecd10adf3.tar.gz jgit-94fad4412ae151c0a71150e8b83edc0ecd10adf3.zip | |
Suppress warning for trying to delete non-empty directory
This is actually a fairly common occurrence; deleting the parent
directories can work only if the file deleted was the last one
in the directory.
Bug: 537872
Change-Id: I86d1d45e1e2631332025ff24af8dfd46c9725711
Signed-off-by: Thomas Wolf <thomas.wolf@paranor.ch>
(cherry picked from commit d9e767b431eae7978613cc8e0ade7467ec04376c)
Signed-off-by: David Pursehouse <david.pursehouse@gmail.com>
Diffstat (limited to 'org.eclipse.jgit.pgm/build.properties')
0 files changed, 0 insertions, 0 deletions