Added handling of ReplaceOption[opt=val]=pretty val. Seems to work.
Description
Description
Details
Details
- Provenance
lonnblad Authored on lonnblad Pushed on Nov 16 2018, 11:25 AM - Parents
- rRIVETHGd7655ca1c3fb: patch rivet-mkhtml for command-line ReplaceOption
- Branches
- Unknown
- Tags