aboutsummaryrefslogtreecommitdiff
path: root/lib/remoteCounter.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-04-13 14:10:33 +0000
committerGitHub2021-04-13 14:10:33 +0000
commitea62d1e19f2ba565ea3a18ba3709a06af5c845ac (patch)
tree3193f7dafa0fc93c1c9b3fc8d47fcc1c2c075f6e /lib/remoteCounter.ml
parentb78e6cfcb412d1c4e5902fb895c5ecaa0cb177ac (diff)
parente1793962bebf1401026ed961ecc15b7eb60d57f5 (diff)
Merge PR #14024: [coqdep] error on non-existent and unreadable files
Reviewed-by: gares Ack-by: jfehrle Ack-by: ejgallego
Diffstat (limited to 'lib/remoteCounter.ml')
0 files changed, 0 insertions, 0 deletions