From 9b1bc18a1fbffef212e53049154b99f64fc8c9ad Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Thu, 23 Mar 2023 08:17:49 +0100 Subject: [PATCH] [headers] header for workspace bench --- .gitattributes | 3 +-- dev/dune-workspace.bench | 22 ++++++++++++++++++++++ headers/headache_config.txt | 4 ++-- 3 files changed, 25 insertions(+), 4 deletions(-) diff --git a/.gitattributes b/.gitattributes index e02a50f0e6e..481e61b451e 100644 --- a/.gitattributes +++ b/.gitattributes @@ -109,6 +109,7 @@ src/plugins/e-acsl/examples/ensuresec/**/*.py -check-indent dune-project header_spec=CEA_LGPL dune header_spec=CEA_LGPL +dune-workspace.* header_spec=CEA_LGPL config* header_spec=CEA_LGPL @@ -198,8 +199,6 @@ README* header_spec=.ignore /bin/sed_get_* header_spec=.ignore -/dev/dune-workspace.* header_spec=.ignore - /dev/docker/*.sh header_spec=.ignore /dev/docker/Dockerfile header_spec=.ignore diff --git a/dev/dune-workspace.bench b/dev/dune-workspace.bench index 87e6d04e0ad..1f5ad5f7195 100644 --- a/dev/dune-workspace.bench +++ b/dev/dune-workspace.bench @@ -1,4 +1,26 @@ (lang dune 3.2) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; +;; This file is part of Frama-C. ;; +;; ;; +;; Copyright (C) 2007-2023 ;; +;; 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). ;; +;; ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (context (default (name bench) diff --git a/headers/headache_config.txt b/headers/headache_config.txt index dc8775f3dfe..da136e6e52e 100644 --- a/headers/headache_config.txt +++ b/headers/headache_config.txt @@ -58,8 +58,8 @@ ######## | "dune-project" -> frame open:";;" line:";" close:";;" | ".*dune-project" -> skip match:"(lang.*" -| "dune-workspace" -> frame open:";;" line:";" close:";;" -| "dune-workspace" -> skip match:"(lang.*" +| "dune-workspace.*" -> frame open:";;" line:";" close:";;" +| ".*dune-workspace.*" -> skip match:"(lang.*" | "dune" -> frame open:";;" line:";" close:";;" ############ -- GitLab