diff options
| author | Enrico Tassi | 2016-05-27 13:13:25 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-05-27 13:13:25 +0200 |
| commit | 34ba7e0d17c76c42a8ece4d195d280f7722f3bae (patch) | |
| tree | 00b803de79f4da35dc4aea3f6b0eb7443ee49ca0 /dev | |
| parent | 7b1e94365bee6cc984e5f476864ac753e6f46e3a (diff) | |
STM: fix argument filtering for slaves
Command line options to be dropped got outdated after vi -> vio renaming.
This made the par: goal selector do not work in conjunction with -quick.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions