diff options
Diffstat (limited to 'erts/etc')
| -rw-r--r-- | erts/etc/unix/cerl.src | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/erts/etc/unix/cerl.src b/erts/etc/unix/cerl.src index cc7d77fd9a..f99059cb72 100644 --- a/erts/etc/unix/cerl.src +++ b/erts/etc/unix/cerl.src @@ -171,6 +171,11 @@ while [ $# -gt 0 ]; do cargs="$cargs -debug" TYPE=.debug ;; + "-frmptr") + shift + cargs="$cargs -frmptr" + TYPE=.frmptr + ;; "-gdb") shift GDB=gdb |