diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-22 11:42:18 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-22 11:42:18 -0700 |
| commit | 2497ad1ab15dfc888720b84ba9e1c03a411c5dea (patch) | |
| tree | 6bf19763cec7e8b982e3ddf211bec6bfe7f8ce98 /.gitmodules | |
| parent | f6003677e2d58fbfb1364a10d34d838fbfb280e4 (diff) | |
Add coq-scripts submodule for timing scripts
Diffstat (limited to '.gitmodules')
| -rw-r--r-- | .gitmodules | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 000000000..eb73fc298 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "etc/coq-scripts"] + path = etc/coq-scripts + url = https://github.com/JasonGross/coq-scripts.git |