'main': Don't highlight unknown precommand flags as errors.

We cannot now for sure whether the flag is misspelled or simply unknown to us, so err on the side of caution. This fixes an unreleased regression. Fixes #658. Issue #641 was originally filed about this problem, but is left open to track further enhancements.
2020-01-12 15:53:59 +00:00
parent 3a6f7e7bfe
commit 5012d771f3
3 changed files with 6 additions and 9 deletions
--- a/highlighters/main/test-data/precommand-unknown-option.zsh
+++ b/highlighters/main/test-data/precommand-unknown-option.zsh
@@ -38,6 +38,6 @@ expected_region_highlight=(
  '10 11 command' # ls
  '12 12 commandseparator' # ;
  '14 17 precommand' # sudo
-  '19 20 unknown-token' # -x
-  '22 23 command' # ls
+  '19 20 single-hyphen-option' # -x
+  '22 23 default' # ls
 )