fix GAPDoc syntax for the manual in `doc/dev` (#5825) #5786

Job	Run time
testinstall - - ubuntu-latest	4m 45s
Cross compiler for s390x	27m 9s
Test in OpenBSD	8m 11s
teststandard - - ubuntu-latest	19m 32s
testmanuals - - ubuntu-latest	5m 52s
testexpect testmockpkg testspecial test-compile testlibgap testkernel testworkspace - - ubuntu-latest	6m 46s
testpackages testinstall-loadall - - ubuntu-latest	26m 44s
makemanuals testmakeinstall - CONFIGFLAGS="--prefix=/tmp/gapprefix" NO_COVERAGE=1 - ubuntu-latest	5m 49s
teststandard - ABI=32 CONFIGFLAGS="" - ubuntu-20.04	18m 6s
testinstall - HPCGAP=yes ABI=64 - ubuntu-latest	7m 49s
testmockpkg testinstall - BOOTSTRAP_MINIMAL=yes - macos-latest	3m 53s
testbugfix - CONFIGFLAGS="--enable-memory-checking" - ubuntu-latest	28m 7s
testbuildsys testmockpkg testinstall - NO_COVERAGE=1 ABI=64 BUILDDIR=out-of-tree CONFIGFLAGS="--enable-valgrind" - ubuntu-latest	4m 55s
testbuildsys testmockpkg testinstall - NO_COVERAGE=1 ABI=32 BUILDDIR=out-of-tree CONFIGFLAGS="" - ubuntu-20.04	4m 27s
testinstall - JULIA=yes CONFIGFLAGS="--enable-debug --disable-Werror" - ubuntu-20.04	4m 46s
testmockpkg testinstall - - windows-2019	15m 15s
Send Slack notification on status change	5s
	3h 12m 11s

Provide feedback