9631318 Use dist_* instead of duplication in EXTRA_DIST

Authored and Committed by mitr 10 years ago
    Use dist_* instead of duplication in EXTRA_DIST