[isabelle-dev] Sum_of_Powers and "potential disaster"

Makarius makarius at sketis.net
Fri Aug 26 16:13:14 CEST 2022

On 26/08/2022 13:45, Lawrence Paulson wrote:
> I finally deleted HOL-ex.Sum_of_Powers. The testboard job eventually failed with the following message, which I’ve seen a lot lately, so I assume it’s irrelevant to my change.

> Presentation in "/media/data/jenkins/workspace/testboard/browser_info"
> 01:40:34 *** Existing content in "/media/data/jenkins/workspace/testboard/browser_info" lacks ".browser_info" meta data.
> 01:40:34 *** To avoid potential disaster, it has not been changed automatically.
> 01:40:34 *** If this is the intended directory, please move/remove/empty it manually.
> 01:40:35 Build step 'Execute shell' marked build as failure

I wrote this exceedingly explicit error message to avoid additional 
documentation and explanations.

Someone with access to the Jenkins setup needs to do what the messages says.


More information about the isabelle-dev mailing list