diff options
| author | coqbot-app[bot] | 2021-02-11 23:32:01 +0000 |
|---|---|---|
| committer | GitHub | 2021-02-11 23:32:01 +0000 |
| commit | c0e0e637c61e075f43b73d1ddd8eaa9d79b27561 (patch) | |
| tree | ce95c0dffc03c16e41590a2d435d5e949e3c9654 /dev/ci | |
| parent | b1532790555b122b5bb3091405595b4b5586483e (diff) | |
| parent | 0a88e8ffeec97768096a32ad1cdd886103aaf30a (diff) | |
Merge PR #13844: [vernac] pass the loc of the whole command to the interp function
Reviewed-by: ejgallego
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/13844-gares-command-loc.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/13844-gares-command-loc.sh b/dev/ci/user-overlays/13844-gares-command-loc.sh new file mode 100644 index 0000000000..d9a1736532 --- /dev/null +++ b/dev/ci/user-overlays/13844-gares-command-loc.sh @@ -0,0 +1 @@ +overlay elpi https://github.com/LPCIC/coq-elpi command-loc 13844 |