Add support for non-string options when scheduling tasks.
This also fixes the pretty-printing of tasks, which was ambiguous
(42 and "42" where both printed as 42).
Description
Description
Details
Details
- Provenance
vlorentz Authored on Mar 13 2019, 9:57 AM vlorentz Pushed on Mar 13 2019, 9:57 AM - Differential Revision
- D1195: Add support for non-string options when scheduling tasks.
- Build Status
Buildable 4614 Build 6121: test-and-build