diff options
Diffstat (limited to 'dune-version.diff')
| -rw-r--r-- | dune-version.diff | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/dune-version.diff b/dune-version.diff new file mode 100644 index 000000000000..e02860cf93bd --- /dev/null +++ b/dune-version.diff @@ -0,0 +1,10 @@ +diff --git a/dune-project b/dune-project +index 9efd891..c99bd5e 100644 +--- a/dune-project ++++ b/dune-project +@@ -1,4 +1,4 @@ +-(lang dune 2.0) ++(lang dune 1.11) + (name visitors) + (version 20200210) + (package |