Fix deprecation of NoFramePointer
-- 08 April 2018
- api.deprecateValue("flags", "NoFramePointer", 'Use `framepointer "Off"` instead.',
+ api.deprecateValue("flags", "NoFramePointer", 'Use `omitframepointer "On"` instead.',
function(value)
omitframepointer("On")
+ end,
+ function(value)
+ omitframepointer("Default")
end)
-----------------------------------------------------------------------------
