master rewritten


We needed to rewrite the history of the last 61 commits of the master.
As you know this is the first time we had to do this, and we are not
planning on making this a regular event.

Commit 3dfda9a5f57e00bfe6f1816c4acdec656c41a14d introduced unwanted
files. They were excessively large and e.g. refused by github.

I have rewritten 3dfda9a5f57e00bfe6f1816c4acdec656c41a14d~1…HEAD (i.e.
as 5941218ebc4c00fb409e3b75c584550611e003db~1…HEAD (i.e.
to filter them out of the commits:

$ git filter-branch --tree-filter ‘rm -rf .vscode’ 3dfda9a~1…HEAD


(And yes, these files are .gitignored since.)

You will see, upon a git pull of the master from, the message:

  • 38b1c0e…e024758 master -> root/master (forced update)
    Our github mirror is not affected as it stopped to sync due to the
    relevant commit.

Apologies for the inconvenience this might have caused.

Cheers, Axel.