aboutsummaryrefslogtreecommitdiff
path: root/etc
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-04-15 17:43:39 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-04-15 17:43:39 -0400
commita90c2b5eeed88e611b241dc1a52cb94f92bb40e7 (patch)
tree5013d1bea2e8424c894a14d308c99516771b9d3b /etc
parent8b80c0547a1c2d28af8d7b24a4ee03962c45e3ff (diff)
Bump coq-scripts to fix a bug
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
-Subproject 5dc2bd6dca55c89d9305672252ab4380e5a9550
+Subproject ef2d7f9e7e9530f05fb3b2362db787a2885c59b