language-servers/erg
1
0
Fork 0
mirror of https://github.com/erg-lang/erg.git synced 2025-08-24 12:24:37 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Update docs

Browse source
This commit is contained in:
Shunsuke Shibayama 2023-01-26 13:45:23 +09:00
parent 4b08fd21a2
commit cbaf48c04b
13 changed files with 164 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

23
doc/scripts/align_files.py Normal file
View file

@ -0,0 +1,23 @@
import os
import glob
"""
Align file prefixes when they are not numbered consecutively.
existing files: 01_foo.md, 03_bar.md, 04_baz.md
result: 01_foo.md, 02_bar.md, 03_baz.md
"""
if __name__ == '__main__':
prev = None
diff = None
for f in sorted(glob.glob("[0-9][0-9]_*")):
if prev != None:
now_file_no = int(f.split("_")[0])
diff = now_file_no - prev
if diff != 1:
replace_to = "_".join([f"{now_file_no-diff+1:02d}", *f.split("_")[1:]])
os.rename(f, replace_to)
prev = now_file_no - diff + 1
else:
prev = now_file_no
else:
prev = int(f.split("_")[0])