aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-28 14:38:57 +0000
committerGitHub2020-09-28 14:38:57 +0000
commitbd24f72a06343b375ad20aaa5b7296c2ad904a5c (patch)
tree0aefe90fa9925755b7eecb9c63b693c772f1a523 /interp
parentb9f385cb43de4c463e649f8f6e33f32288e88a6c (diff)
parent424ae427197126a2fcbd5f07eaa181fb6f81ad84 (diff)
Merge PR #13105: [nix] CI script wrapper now requires Python
Reviewed-by: vbgl
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions