diff options
| author | Emilio Jesus Gallego Arias | 2020-07-02 18:56:01 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-08-27 18:59:47 +0200 |
| commit | 60d2e06769abee8e7ebc9b9cc9febf05c8f8994a (patch) | |
| tree | dbb8f576471b044dd65724dc10a85dcef519ffbb /Makefile.dev | |
| parent | a87c09c13028502ea86a553724a4131c5246145a (diff) | |
[state] A few nits after consolidation of state.
We remove some dead aliases and add some documentation to the
interface file.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions