diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 15:55:56 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 15:55:56 +0100 |
commit | a15ae330fd156b74fcdfb4fc39b79013d3e398bf (patch) | |
tree | df52975748b4e5737385589788482ad057d1e937 /library/globnames.ml | |
parent | 972c0e941a8acdd33053e2032ae0401b9aa4605d (diff) | |
parent | e849572cd2b242b34fbec6c3eaa42e7d2e7cc550 (diff) |
Merge PR #6685: Use whd-all on rigid-flex conversion.
Diffstat (limited to 'library/globnames.ml')
0 files changed, 0 insertions, 0 deletions