help consumes next command

Stream: mathlib4

[Floris van Doorn]

import Mathlib.Tactic.HelpCmd

#help tactic -- Error: no tactic declarations start with def

def x := 1

Note: this is not just the case for def, but seems to be the behavior for all commands that don't start with #.