Diff result files on host, do not rely on diff being available on device#142

Merged

hevrard merged 1 commit intomasterfrom diff-on-host

Nov 28, 2018

+22-19

Commits on Nov 28, 2018

Diff result files on host, do not rely on diff being available on device
hevrard
committed