dune.inc files not handled #50
Description
dune.inc files are not handled. Not sure if such name are a just a convention, or if such extension is expected. It looks like include would accept any filename.
{{ message }}
dune.inc files are not handled. Not sure if such name are a just a convention, or if such extension is expected. It looks like include would accept any filename.