Merge pull request #1771 from jnpkrn/fix-make-dist
Fix "make dist" wrt. doc
Description
Description
Details
Details
- Provenance
kgaillot Authored on May 10 2019, 5:24 PM GitHub <noreply@github.com> Committed on May 10 2019, 5:24 PM - Parents
- rP72cfbc6b9458: Build: fix "make dist" in one go deficiency (and if, it's brokenness)
rP7b56968c586a: Merge pull request #1772 from gao-yan/confirm-cancel-of-failed-monitor - Branches
- Unknown
- Tags
Event Timeline
Merged Changes
Merged Changes