aboutsummaryrefslogtreecommitdiff
path: root/etc/NOTICE
diff options
context:
space:
mode:
authorEnrico Tassi2015-03-09 13:35:08 +0100
committerEnrico Tassi2015-03-09 16:21:23 +0100
commit155e671f7b83293ae327ddbd252d1d1ac961ab9a (patch)
tree7bb826abaa20f3fe5ac57e0348be14e8641b5b75 /etc/NOTICE
parentfc84c27eac260dffd8f2fb1cb56d599f1e3486d9 (diff)
some work on ssreflect and discrete
Diffstat (limited to 'etc/NOTICE')
-rw-r--r--etc/NOTICE2
1 files changed, 2 insertions, 0 deletions
diff --git a/etc/NOTICE b/etc/NOTICE
new file mode 100644
index 0000000..a8dd3a6
--- /dev/null
+++ b/etc/NOTICE
@@ -0,0 +1,2 @@
+(* (c) Copyright Microsoft Corporation and Inria. *)
+(* You may distribute this file under the terms of the CeCILL-B license *)