Reverting wrong change to build_docs.sh... forgot what "make source" was for.
Authored by: m0slevin 2014-03-30
Parent: [r171]
Child: [r173]