michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(ltags): support .hlean files

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-05 16:25:43 -08:00
parent effbf78d36
commit 2306c14337
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
bin/ltags
View file

@ -175,11 +175,12 @@ def find_makefile_upward(path, makefile_names):
return False
def filter_ilean_files(ilean_files):
"""Remove .ilean file if a corresponding .lean file does not exist."""
"""Remove .ilean file if a corresponding .lean/.hlean file does not exist."""
result = []
for ilean_file in ilean_files:
lean_file = ilean_file[:-5] + "lean"
if os.path.isfile(lean_file) and os.path.isfile(ilean_file):
hlean_file = ilean_file[:-5] + "hlean"
if (os.path.isfile(lean_file) or os.path.isfile(hlean_file)) and os.path.isfile(ilean_file):
result.append(ilean_file)
return result