Merge pull request #13110 from pgavlin/SPMIJitOptions
authorPat Gavlin <pgavlin@gmail.com>
Sat, 9 Sep 2017 04:14:13 +0000 (21:14 -0700)
committerGitHub <noreply@github.com>
Sat, 9 Sep 2017 04:14:13 +0000 (21:14 -0700)
Add the capability to specify JIT options on the SPMI command line.


Trivial merge