Looking at 99eba20#diff-fee45415ce1a1c290e697917da2b716532bcff66dbe1d9ae5caea30144bb0cc3, it's unclear what was the original docs file edited, and which are autogenerated:

• MANUAL
• MANUAL.markdown
• doc/manual.html

Which file does one edit, and which make commands does one then run?