bin: tooling and documentation about option names

* src/bin/options.py: New file.
* src/bin/Makefile.am: Distribute it.
* src/bin/README: New file.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-29 23:42:06 +01:00
parent 21dcc73deb
commit 18d8c3efc0
3 changed files with 125 additions and 0 deletions

View file

@ -64,3 +64,5 @@ ltlgrind_SOURCES = ltlgrind.cc
dstar2tgba_SOURCES = dstar2tgba.cc
spot_x_SOURCES = spot-x.cc
ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME)
EXTRA_DIST = options.py