diff options
| author | Pierre-Marie Pédrot | 2020-04-01 17:39:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-10 15:04:06 +0200 |
| commit | cf60564b9e6cdfa35fe8c256f6785e23a2afde61 (patch) | |
| tree | c647d30d9d8ed572ff43717c09f0d0c55356cb9a /dev | |
| parent | 2a79abc613bdf19b53685a40c993f964455904fe (diff) | |
Further cleanup: remove the local_reduction_function type.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions