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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
