`@@NoJit` sounds pretty alright to me. On Mon, Aug 3, 2020, 11:27 PM Derick Rethans <der...@php.net> wrote:
> On 3 August 2020 20:20:35 BST, Benjamin Eberlei <kont...@beberlei.de> > wrote: > > >In that case maybe we should rename the attribute to @@DisableJit ? > >This > >would not clutter the global namespace with a "jit" class. > > Things with a negative name are usually a code smell. I'm not keen on a > @[disableJit] attribute name. > > cheers, > Derick > > -- > PHP Internals - PHP Runtime Development Mailing List > To unsubscribe, visit: https://www.php.net/unsub.php > >
