diff options
| author | Jason Gross | 2019-02-16 19:44:39 +0100 |
|---|---|---|
| committer | GitHub | 2019-02-16 19:44:39 +0100 |
| commit | 0e82d6b1a3006ad260e91c06be9151bfdd406f8e (patch) | |
| tree | 95a4d5f7f1d806d10189331df1ce26a1725d1cf6 /dev/include_dune | |
| parent | 2533f5ca0eea4ceb7d1cae3b91be3be2eb525ede (diff) | |
Fix English grammar.
Co-Authored-By: Zimmi48 <theo.zimmermann@univ-paris-diderot.fr>
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions