In particular, this fixes the outdated @source tooltip for local imports. Moreover, headlines in the execution pabel have lost their superfluous : and the Run headline is gone (the button says that already).
Please check that layout is looking good in browser before merging.
In particular, this fixes the outdated
@sourcetooltip for local imports. Moreover, headlines in the execution pabel have lost their superfluous:and theRunheadline is gone (the button says that already).Please check that layout is looking good in browser before merging.