NoRedInk/noredink-ui
1
1
Fork 0
mirror of https://github.com/NoRedInk/noredink-ui.git synced 2024-11-04 07:02:12 +03:00
Code Issues Packages Projects Releases Wiki Activity

do the right thing when handling a broken symlink

Browse Source
This commit is contained in:
Brian Hicks 2023-05-02 10:44:33 -05:00
parent 5f2937c188
commit 36f4ec1da0
No known key found for this signature in database
GPG Key ID: C4F324B9CAAB0D50
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
prelude-nri/elm/isolated_compile.py
View File

@ -22,7 +22,7 @@ def symlink_if_necessary(source, target):
- If the target already exists and points somewhere else, remove it
and relink.
"""
if os.path.exists(target):
if os.path.lexists(target):
if os.path.isfile(target):
logging.debug(f"`{target}` is a regular file")