Commit 5663e8aa authored by MARCHE Claude's avatar MARCHE Claude

fix headers

parent 0f6fe364
......@@ -1810,9 +1810,10 @@ $(DISTRIB_TAR): doc/manual.pdf
headers:
headache -c misc/headache_config.txt -h misc/header.txt \
Makefile.in configure.in src/*.ml* src/*/*.ml* \
plugins/*/*.ml* src/tools/cpulimit.c \
examples/use_api/*.ml*
Makefile.in configure.in src/*.ml \
src/*/*.ml src/*/*.ml[iyl] \
plugins/*/*.ml plugins/*/*.ml[ily] src/tools/cpulimit.c \
examples/use_api/*.ml
#########
# myself
......
......@@ -207,7 +207,7 @@ Scheduled for 9 december 2013
* faire une passe sur le BTS
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK
* check that "make xml-validate" is OK
* check that "make xml-validate-local" is OK
(see below : copy the dtd on the web)
* put 0.82 in file Version
* check headers
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2013 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
{
open Why3
......
......@@ -9,8 +9,8 @@
(* *)
(********************************************************************)
(** Isabelle printer
main author: Stefan Berghofer <stefan.berghofer@secunet.com>
(** Isabelle printer
main author: Stefan Berghofer <stefan.berghofer@secunet.com>
*)
open Format
......@@ -470,10 +470,10 @@ let print_task printer_args realize fmt task =
((thname, opt_string_of_bool realize),
(Mid.values realized_theories, local_decls))
let print_task_full args ?old fmt task =
let print_task_full args ?old:_ fmt task =
print_task args false fmt task
let print_task_real args ?old fmt task =
let print_task_real args ?old:_ fmt task =
print_task args true fmt task
let () = register_printer "isabelle" print_task_full
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Format
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment