antiquotations in docstrings

Stream: lean4

[Edward Ayers]

Hi how can I use antiquotations in docstrings?

elab "make_foo" decl:ident : command => do
  elabCommand <|← `(
      /-- Docstring for $decl docstring $(mkIdent `hello) -/
      def $decl : Nat := 5
  )

make_foo foo

#check foo

If I hover over foo it will show me the docstring but unfortunately the antiquotes just show as the literal$decl. Is there a special antiquote for comments?