@ctrl should not be a command at all. See the NEWS for 3.8 (1996),
below. All that C makeinfo does with (some of) them is say "@CMD is
obsolete". I think we can safely remove them all at this point, unless
you think otherwise.
Thanks,
k
* Deprecate these obsolete commands, to be removed in the next release:
@ctrl
@infoinclude
@iappendix @iappendixsection @iappendixsec @iappendixsubsec
@iappendixsubsubsec
@ichapter @isection @isubsection @isubsubsection
@iunnumbered @iunnumberedsec @iunnumberedsubsec @iunnumberedsubsubsec
@setchapterstyle
@titlespec
