Change `WorkProduct::saved_files` to an `Option`.#72126

Merged

bors merged 1 commit intorust-lang:masterfrom

nnethercote:change-WorkProduct-saved_files

May 14, 2020

Commits on May 12, 2020

Change `WorkProduct::saved_files` to an `Option`.
nnethercote
committed