Merge pull request #234 from berkerpeksag/disable-docs
authorTom Tromey <tom@tromey.com>
Tue, 17 May 2016 23:07:27 +0000 (17:07 -0600)
committerTom Tromey <tom@tromey.com>
Tue, 17 May 2016 23:07:27 +0000 (17:07 -0600)
Add a note about the --disable-docs switch


Trivial merge