Merge branch 'rubi-misc'
This is old misc stuff that I rebased yesterday. Actually, I had more moves to fsm-lib, but some of it already moved to common-fun (which I dislike, but let's ignore the thing by now).
Showing
Please
register
or
sign in
to comment