diff options
| author | Emilio Jesus Gallego Arias | 2019-04-27 15:37:09 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-29 07:11:04 +0000 |
| commit | 4f2da48207010b5edca8f0a9a4c5afe7e10eec17 (patch) | |
| tree | 264d39a9a8bbe69ff98d7c7c7038d6972d2e2ad8 /lib | |
| parent | f1fd3d42d87f8b9dd840c613dad235e3b5f3338e (diff) | |
[meta] [dune] Fix discrepancies in plugin names
We have some discrepancy with the package names for plugins in the
META / Dune case. This PR fixes it.
At some point there was a need for plugin package names having to be
named as their directories.
I think this is not true anymore, but taking the "dir_name ==
package_name" convention just in case.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions