aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-03-11 11:57:46 +0000
committerGitHub2021-03-11 11:57:46 +0000
commitd33266649d285b7d8ba5a7093319faa6132d6bc9 (patch)
treea49c779eeddeb56909d3dd85f8423fde133a88fb /Makefile.dev
parenta40631f9fbcd0ef8c1a716010be48e3f650e8955 (diff)
parentb31c4fa57eac8162ad6b6e03f75b13afd9b76db7 (diff)
Merge PR #13854: Normalize evars during bytecode compilation.
Reviewed-by: SkySkimmer Ack-by: ppedrot Ack-by: ejgallego
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions