[isabelle-dev] Sum_of_Powers and "potential disaster"
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