diff options
author | Thomas Wolf <thomas.wolf@paranor.ch> | 2018-08-19 20:48:06 +0200 |
---|---|---|
committer | Thomas Wolf <thomas.wolf@paranor.ch> | 2018-08-22 18:36:31 +0200 |
commit | d9e767b431eae7978613cc8e0ade7467ec04376c (patch) | |
tree | 32ae3978f1924628c3b355702bb1b167deda0191 /org.eclipse.jgit.packaging | |
parent | ffd1ac5dde053e861ad249d7d8d27df7cef56eb9 (diff) | |
download | jgit-d9e767b431eae7978613cc8e0ade7467ec04376c.tar.gz jgit-d9e767b431eae7978613cc8e0ade7467ec04376c.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>
Diffstat (limited to 'org.eclipse.jgit.packaging')
0 files changed, 0 insertions, 0 deletions