80d21dc Revert "Simplify the build-docs target"

Authored and Committed by mgrepl 12 years ago
    Revert "Simplify the build-docs target"
    
    This reverts commit 01be4862923cef936acb3e6b599295028b6e16ec.
    
        
file modified
+5 -4