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

chore: update docs/scripts

Browse source
This commit is contained in:
Shunsuke Shibayama 2023-02-12 12:31:40 +09:00
parent b1a3e97334
commit 8495bd3570
3 changed files with 6 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

9
doc/scripts/mylib.py
View file

@ -11,12 +11,3 @@ path_join = os.path.join
def str_slice(str: str, first_index: int):
return str[first_index:]
def eliminate_none_on_match(matched: re.Match):
class _a:
def __init__(self):
self.matched = matched
self.is_none = True if matched is None else False
return _a()