[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