<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>Hi,
</p>
    <div class="moz-cite-prefix">Am 25.01.2022 um 11:50 schrieb Thorsten
      Otto via fpc-devel:<br>
    </div>
    <blockquote type="cite" cite="mid:5601929.rBMcL6byi9@earendil">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <meta name="qrichtext" content="1">
      <style type="text/css">p, li { white-space: pre-wrap; }</style>
      <p style=" margin-top:0px; margin-bottom:0px; margin-left:0px; margin-right:0px; -qt-block-indent:0; text-indent:0px; -qt-user-state:0;">On Dienstag, 25. Januar 2022 11:27:11 CET Marcus Sackrow via fpc-devel wrote:</p>
      <p style=" margin-top:0px; margin-bottom:0px; margin-left:0px; margin-right:0px; -qt-block-indent:0; text-indent:0px; -qt-user-state:0;">> hmm what do you mean? I wrote it, of course.</p>
      <p style="-qt-paragraph-type:empty; margin-top:0px; margin-bottom:0px; margin-left:0px; margin-right:0px; -qt-block-indent:0; text-indent:0px; "> </p>
      <p style=" margin-top:0px; margin-bottom:0px; margin-left:0px; margin-right:0px; -qt-block-indent:0; text-indent:0px; -qt-user-state:0;">But is that a script that is stored somewhere, or is it just a setting inside your Jenkins installation?</p>
    </blockquote>
    <p>
</p>
    <p>yes, thats how jenkins work usually, it comes with an building editor to write the script. But the script is not very fancy or complicated.</p>
    <p>It's just that "make" line and afterwards copy the archive to webspace and copy some other stuff for the online compiler</p>
    <p>at the end cleanup to save space</p>
    <p>
</p>
    <p>Greetings,</p>
    <p>Marcus
</p>
  </body>
</html>