summaryrefslogtreecommitdiff
path: root/demo/tree.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2013-12-09 15:47:14 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2013-12-09 15:47:14 -0500
commitdb0aff13453186d3f6edf46b42e43690ea113aea (patch)
treee034f612a841d48eb9db72b593b77bd4c07c909e /demo/tree.urs
parentfa448e6a07ce4435d596019497a3da8e4eb33f23 (diff)
Rename <activeHead> to <script> and make it work properly
Diffstat (limited to 'demo/tree.urs')
0 files changed, 0 insertions, 0 deletions