diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2013-12-09 15:47:14 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2013-12-09 15:47:14 -0500 |
| commit | db0aff13453186d3f6edf46b42e43690ea113aea (patch) | |
| tree | e034f612a841d48eb9db72b593b77bd4c07c909e /demo/tree.urs | |
| parent | fa448e6a07ce4435d596019497a3da8e4eb33f23 (diff) | |
Rename <activeHead> to <script> and make it work properly
Diffstat (limited to 'demo/tree.urs')
0 files changed, 0 insertions, 0 deletions