Commit a44a5b863aaae98041e11aa3256907bf912ee4d6

Tom Tromey 2016-05-17T17:07:27

Merge pull request #234 from berkerpeksag/disable-docs Add a note about the --disable-docs switch