aboutsummaryrefslogtreecommitdiffstats
path: root/tools/ndfun.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-17 18:28:55 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-17 18:28:55 +0100
commita1c401a4eba5fc9fcf42933f70005ecb679a4c1c (patch)
tree26637fca5d1da9b3d049234721d593a60b03a6d3 /tools/ndfun.ml
parentc49caca4b5f0239b43610fbfe012d6ba0211b364 (diff)
parent1daf96cdca4d828c333cea5c9a314ef861342984 (diff)
downloadcompcert-a1c401a4eba5fc9fcf42933f70005ecb679a4c1c.tar.gz
compcert-a1c401a4eba5fc9fcf42933f70005ecb679a4c1c.zip
Merge branch 'master' into dev/michalisdev/michalis
Diffstat (limited to 'tools/ndfun.ml')
-rw-r--r--tools/ndfun.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/tools/ndfun.ml b/tools/ndfun.ml
index b6a87ede..3e3daad2 100644
--- a/tools/ndfun.ml
+++ b/tools/ndfun.ml
@@ -6,10 +6,11 @@
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the GNU General Public License as published by *)
-(* the Free Software Foundation, either version 2 of the License, or *)
-(* (at your option) any later version. This file is also distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* under the terms of the GNU Lesser General Public License as *)
+(* published by the Free Software Foundation, either version 2.1 of *)
+(* the License, or (at your option) any later version. *)
+(* This file is also distributed under the terms of the *)
+(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)