python: rename aux.py to aux_.py
Fixes #437, reporeted by Yann Thierry-Mieg. * python/spot/aux.py: Rename as... * python/spot/aux_.py: ... this. * python/spot/__init__.py, python/Makefile.am: Adjust. * NEWS: Mention the change.
This commit is contained in:
parent
14a992bb89
commit
ffc0138ed6
4 changed files with 18 additions and 3 deletions
|
|
@ -30,7 +30,7 @@ SWIGFLAGS = -c++ -python -py3 -O -MD
|
|||
EXTRA_DIST = buddy.i spot/impl.i spot/ltsmin.i spot/gen.i
|
||||
nobase_pyexec_PYTHON = \
|
||||
spot/__init__.py \
|
||||
spot/aux.py \
|
||||
spot/aux_.py \
|
||||
spot/impl.py \
|
||||
spot/ltsmin.py \
|
||||
spot/gen.py \
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue