2ebc5f097b
This helps distro packagers avoid having to create a directory with the generic `plugin` name in system locations. Context: https://github.com/deepmind/mujoco/issues/552 PiperOrigin-RevId: 489011386 Change-Id: Ie9f1748cbb4f2b9dc8c328064caaeb50c88fdec3