The warning introduced with !633 (merged) produces false positives when unpickling options.
I introduced a protection to prevent warnings when unpickling.
Marco Clemencic authored
Marco Clemencic authored