diff options
| author | Emilio Jesus Gallego Arias | 2020-03-15 17:08:16 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:37 -0400 |
| commit | f836b601e3cb81dd24d25ccd910b2506aac998d9 (patch) | |
| tree | 2be52d61cf4ad8b00a9c9b487b340808a3c5ad11 /doc/plugin_tutorial/Makefile | |
| parent | fa6836e85808c6d97620104b2f33dff49eb2aa74 (diff) | |
[program] Use common type for fixpoint declarations.
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions