Commit ebd1930207615f7ae900ac108b84e1ae6683ca81

DRC 2022-03-10T23:21:55

GitHub Actions: "linux-12bit" --> "linux-no12bit" This job tests the non-default value of WITH_12BIT, which is now 0 instead of 1.