diff options
| author | Pierre-Marie Pédrot | 2021-03-05 19:04:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-05 19:04:27 +0100 |
| commit | aacf8f1756fa5a289f27485a1951392505edfc53 (patch) | |
| tree | ab18d66b36858bb17dff02b041e9b5817cdb9a5c /dev | |
| parent | b016348348f8b2dfaaf19c3a46436261a0ebde42 (diff) | |
| parent | 303941d805efe6d02273afa099fac74cc0efbf90 (diff) | |
Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/13842-proux01-remove-decimal.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/13842-proux01-remove-decimal.sh b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh new file mode 100644 index 0000000000..5ede8221ce --- /dev/null +++ b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh @@ -0,0 +1 @@ +overlay hott https://github.com/proux01/HoTT coq-13842 13842 |