History | View | Annotate | Download (20.6 kB)
Add CLI-level option to override the priority
This just defined the new priority, with the same name as the Python one.
Signed-off-by: Iustin Pop <iustin@google.com>Reviewed-by: Guido Trotter <ultrotter@google.com>
CLI.hs: fix double spaces in option help strings
Some help strings with continuation backslashes ('\') were providing aspace both before and after the backslash, resulting in double spaces inhelp output. Provide it only after the backslash, which fixes the issue and...
Rename htools/ to src/
Per offline discussions, this is the first patch of therenames. Tested with "make distcheck", seems to work fine.
The only change outside of the renaming is a bit of simplification inthe .gitignore rules; otherwise, simply s/htools/src/....