diff options
Diffstat (limited to 'developer/emir/custom.properties')
| -rw-r--r-- | developer/emir/custom.properties | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/developer/emir/custom.properties b/developer/emir/custom.properties new file mode 100644 index 0000000000..7d21fd20e1 --- /dev/null +++ b/developer/emir/custom.properties @@ -0,0 +1,2 @@ +nscArgs = -check:term;-check:transmatch;-debug + |