summaryrefslogtreecommitdiff
path: root/demo/noisy.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 17:25:09 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 17:25:09 -0400
commit76a1338e6d9b75a03c7741f2c0df827043c97b34 (patch)
tree7e42609843840dee056822c9068c7b5758196e1f /demo/noisy.urs
parent486c4f75cb34e0c9aa4069fda1595c722da38d07 (diff)
Allow HTML in tutorial comments
Diffstat (limited to 'demo/noisy.urs')
0 files changed, 0 insertions, 0 deletions