aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/pre-commit
diff options
context:
space:
mode:
authorBESSON Frederic2020-11-02 18:46:37 +0100
committerBESSON Frederic2020-11-18 09:49:22 +0100
commit38e836a128d41a5de7dd72f1bf84f6350099aa43 (patch)
treec1e3e60d928a2255c0a1462d94a9ca7a0fbc555f /dev/tools/pre-commit
parent06a70885fe1ed03b6e71a7a0a1123db3074bcdeb (diff)
[micromega] Sort constraints before performing `subst`
This will be more predictable. In case there are several possible substitution, the "simplest" is prefered.
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions