You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I have pushed an initial fix. @Skillmon asks if this should include zapping spaces in the unused option name: I am not so sure so I've not done that yet. Thoughts welcome.
Brief outline of the bug
As title: the behaviour is inconsistent with classical option processing.
Minimal example showing the bug
Log file (required) and possibly PDF file
test.log
The text was updated successfully, but these errors were encountered: