add Event; use it to fix race in Distributed setup#29623
Merged
JeffBezanson merged 2 commits intomasterfrom jb/syncdistributedOct 19, 2018
+78-3
Event; use it to fix race in Distributed setup#29623