diff options
| author | Pierre Roux | 2020-10-20 19:07:22 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:53 +0100 |
| commit | da7787ff4f1b5192b5465ca17ece64f5ebd4f72a (patch) | |
| tree | 14b0a006b87ea609eb2fee81c4e2bd89afc2afb8 /test-suite/output/StringSyntax.out | |
| parent | b6214bd4d5d3003e9b60411a717e84277feead24 (diff) | |
Allow multiple primitive notation on the same scope and triggers
Until now, declaring a number or string notation on some trigger
removed all previous notations on the same scope.
Bug discovered by Jason Gross while reviewing #12218.
Diffstat (limited to 'test-suite/output/StringSyntax.out')
| -rw-r--r-- | test-suite/output/StringSyntax.out | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index 125c1bc927..68ee7cfeb5 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -1096,3 +1096,9 @@ Expects a single character or a three-digit ASCII code. : nat The command has indeed failed with message: Expects a single character or a three-digit ASCII code. +"abc" + : string2 +"abc" : string2 + : string2 +"abc" : string1 + : string1 |