[Hol-developers] recent change will require annoying update shenanigans

[Michael N. <Mic...@ni...>]

(Of course, you can always checkout a fresh copy.)

You will probably find that svn update gives a message like

svn update
U    tools/build-sequence
D    src/bool
svn: Failed to add directory 'src/bool': an unversioned directory of the same name already exists

When this happens, delete src/bool, with rm -r src/bool  (checking that you haven't got anything important in there of your own; it should only be *.ui type files), and then do svn update again.

Michael