diff options
author | Adam Chlipala <adam@chlipala.net> | 2018-12-14 15:42:59 -0500 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2018-12-14 15:42:59 -0500 |
commit | c1932084390aca19c748da024b7b168c160a3aea (patch) | |
tree | 9a9865eda9aed3d1127eecb332ec799bd8d051cd /doc/intro.ur | |
parent | 720e1cb2c84dfd274fcbfd7bf4974a1c110501cb (diff) |
New .urp option: safeGetDefault
Diffstat (limited to 'doc/intro.ur')
0 files changed, 0 insertions, 0 deletions