macro escape syntax

Stream: lean4

[Anders Christiansen Sørby]

I was trying to run the lean4-alloy project by @Mac using the latest lean4, but I run into a parsing error at Alloy.C.Command.lean

`($[$doc?]? @[extern $symLit:strLit] constant $id $sig)

Producing the error

       > Alloy/C/Command.lean:36:36: error: expected ']'
       > Alloy/C/Command.lean:36:69: error: expected command

Is there some new escape sequence that is missing?

[Sebastian Ullrich]

strLit is now str