Commit 2122b5113994de61c7361b7c75cea183e73b14f5

Daniel Mendler 2019-10-27T19:48:13

manual: don't mention obsolete MP_DIV_SMALL