diff options
Diffstat (limited to 'mujoco-py-gen_wrappers.py.patch')
-rw-r--r-- | mujoco-py-gen_wrappers.py.patch | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/mujoco-py-gen_wrappers.py.patch b/mujoco-py-gen_wrappers.py.patch new file mode 100644 index 000000000000..a67c37d4e8c4 --- /dev/null +++ b/mujoco-py-gen_wrappers.py.patch @@ -0,0 +1,22 @@ +--- mujoco-py-2.0.2.13-gen_wrappers.py.orig 2021-10-31 20:06:55.462019060 -0400 ++++ mujoco-py-2.0.2.13-gen_wrappers.py.new 2021-10-31 20:14:05.987046079 -0400 +@@ -527,7 +527,7 @@ + + + def main(): +- HEADER_DIR = os.path.expanduser(os.path.join('~', '.mujoco', 'mujoco200', 'include')) ++ HEADER_DIR = "/opt/mujoco/include" + HEADER_FILES = [ + 'mjmodel.h', + 'mjdata.h', +@@ -939,6 +939,10 @@ + PyMem_Free(self.ptr) + '''.format(name=name) + extra_set = '' ++ elif name in [ ++ 'mjuiItemSingle', 'mjuiItemMulti', 'mjuiItemSlider', 'mjuiItemEdit' ++ ]: ++ continue + elif name[:2] == 'mj': + extra = ''' + def __cinit__(self): |