diff options
Diffstat (limited to 'curves/dune')
-rwxr-xr-x | curves/dune | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/curves/dune b/curves/dune deleted file mode 100755 index 34c87fb..0000000 --- a/curves/dune +++ /dev/null @@ -1,7 +0,0 @@ -(library - (name curves) - (libraries - tools - matrix - ) - ) |