summaryrefslogtreecommitdiff
path: root/doc/intro.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2018-12-14 15:42:59 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2018-12-14 15:42:59 -0500
commitc1932084390aca19c748da024b7b168c160a3aea (patch)
tree9a9865eda9aed3d1127eecb332ec799bd8d051cd /doc/intro.ur
parent720e1cb2c84dfd274fcbfd7bf4974a1c110501cb (diff)
New .urp option: safeGetDefault
Diffstat (limited to 'doc/intro.ur')
0 files changed, 0 insertions, 0 deletions