fix for pointer size when casting to integer in the debugger
Merge pull request #1452 from AntonioBL/pointer_size

fix for pointer size when casting to integer in the debugger