aboutsummaryrefslogtreecommitdiff
path: root/etc
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-06-22 11:42:18 -0700
committerGravatar Jason Gross <jagro@google.com>2016-06-22 11:42:18 -0700
commit2497ad1ab15dfc888720b84ba9e1c03a411c5dea (patch)
tree6bf19763cec7e8b982e3ddf211bec6bfe7f8ce98 /etc
parentf6003677e2d58fbfb1364a10d34d838fbfb280e4 (diff)
Add coq-scripts submodule for timing scripts
Diffstat (limited to 'etc')
m---------etc/coq-scripts0
1 files changed, 0 insertions, 0 deletions
diff --git a/etc/coq-scripts b/etc/coq-scripts
new file mode 160000
+Subproject d858db1f3a64ea683e46204d0d8f775c5dbff97