Jakob Ketterl 97ace65537 don't specify the input paramter ... * version 0.20 of redsea interprets the parameter differently * we can rely on the default for now		2024-01-20 18:38:08 +01:00
..
redsea.py	don't specify the input paramter	2024-01-20 18:38:08 +01:00