[m-rev.] for post-commit review: --deep-std-name
Peter Wang
novalazy at gmail.com
Mon Oct 14 15:56:49 AEDT 2024
On Mon, 14 Oct 2024 12:53:08 +1100 Peter Wang <novalazy at gmail.com> wrote:
> On Mon, 14 Oct 2024 03:41:21 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> >
> >
> > On Mon, 14 Oct 2024 02:02:27 +0200 (CEST), "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> > > > (It would be nice to have a [Reload] command, but this works.)
> > >
> > > I will have a look at that. We could even have *two* reload commands:
> > >
> > > - one that reloads the file with the same name as the profile now displayed, and
> >
> > I just had a look. It seems that we *already* have this command in the usual menu,
> > just called "Restart" instead of "Reload". How does the existing "Restart" action
> > differ from the "Reload" action you want?
>
> Yes, I thought that's what Restart did, but when I tested it again
> today, it didn't load the new profiling data. The Menu and Restart
> actions appear to do the same thing, which obviously wouldn't make
> sense. Maybe it is something to do my setup; I will investigate later.
It's due to commit c6ee55d24 from 2009.
+process_query(Cmd0, DeepFileName0, MaybePref, Options0, !IO) :-
+ ( Cmd0 = deep_cmd_restart ->
+ % This process got started because there was no server, and this
+ % process will become the new server, so the user just got the freshly
+ % started server they asked for. There is no point in starting it
+ % again. As it is, create_report would throw an exception for
+ % deep_cmd_restart, expecting it to be filtered out by its usual caller
+ % server_loop. To avoid the exception, we have to filter it out too.
+ Cmd = deep_cmd_menu
+ ;
+ Cmd = Cmd0
+ ),
Peter
More information about the reviews
mailing list