Merge pull request #129 from jpk15211/hotfix/underscore-signals

Fixed issue with underscore in signal names
This commit is contained in:
Marcell Vazquez-Chanlatte 2019-10-08 19:16:53 -07:00 committed by GitHub
commit cc2b814555
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -44,7 +44,7 @@ interval = "[" __ const_or_unbound __ "," __ const_or_unbound __ "]"
const_or_unbound = const / "inf" / id const_or_unbound = const / "inf" / id
AP = ~r"[a-z][a-z\\d]*" AP = ~r"[a-z_][a-z_\\d]*"
bot = "FALSE" bot = "FALSE"
top = "TRUE" top = "TRUE"