Skip to content

Commit a9864a0

Browse files
authored
if clearing the ports dir fails, show a warning to the user (this can happen if e.g. the user lacks permissions to that directory, and if we don't show this warning, later ports operations may fail as well - when they do, we will suggest clearing ports, so putting the warning here should suffice (#5938)
1 parent 8bfd11a commit a9864a0

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

tools/system_libs.py

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -560,7 +560,10 @@ def get_dir():
560560

561561
@staticmethod
562562
def erase():
563-
shared.try_delete(Ports.get_dir())
563+
dirname = Ports.get_dir()
564+
shared.try_delete(dirname)
565+
if os.path.exists(dirname):
566+
logging.warning('could not delete ports dir %s - try to delete it manually' % dirname)
564567

565568
@staticmethod
566569
def get_build_dir():

0 commit comments

Comments
 (0)