Skip to content

Conversation

Signed-off-by: gabrik <gabriele.baldoni@gmail.com>
Signed-off-by: gabrik <gabriele.baldoni@gmail.com>
@gabrik gabrik merged commit f5195c0 into main May 3, 2024
@gabrik gabrik deleted the chore/rename-no-mangle-to-dynamic-plugin branch May 3, 2024 14:12
YuanYuYuan pushed a commit to ZettaScaleLabs/zenoh that referenced this pull request May 6, 2024
* chore: renamed no_mangle feature to dynamic_plugin

Signed-off-by: gabrik <gabriele.baldoni@gmail.com>

* fix: wrong find and replace fixed

Signed-off-by: gabrik <gabriele.baldoni@gmail.com>

---------

Signed-off-by: gabrik <gabriele.baldoni@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement Existing things could work better

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants