diff options
Diffstat (limited to 'src/config/config_vars.ml.default')
| -rw-r--r-- | src/config/config_vars.ml.default | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/config/config_vars.ml.default b/src/config/config_vars.ml.default new file mode 100644 index 0000000..1b56c41 --- /dev/null +++ b/src/config/config_vars.ml.default @@ -0,0 +1,7 @@ +type 'a value = + | This of 'a + | Auto + +let enable_zlib = Auto + +let enable_hardware_support = Auto |