Devil's manual is inaccessible from Info. The reason is that MANUAL.org sets the dir title (or id or whatever) to devil-mode, but exports to MANUAL.info. It needs to be fixed. And by the way, it'll probably a better fit if you set the dir title to devil.
Devil's manual is inaccessible from Info. The reason is that MANUAL.org sets the dir title (or id or whatever) to
devil-mode
, but exports toMANUAL.info
. It needs to be fixed. And by the way, it'll probably a better fit if you set the dir title todevil
.