{
    casesensitive.true=(Unix);
    casesensitive.false=(Windows,MacOS);
}
