From a6b13a81c4710b6710d27ffedaf106d0e7fe374b Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Wed, 26 Oct 2022 16:02:46 +0200 Subject: [PATCH] [hdrck] typos --- Makefile | 2 +- tools/hdrck/dune-project | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 7a62602f3ae..ab760d6563c 100644 --- a/Makefile +++ b/Makefile @@ -81,7 +81,7 @@ include ivette/Makefile.installation ################################ # HDRCK is internal -FRAMAC_HDRCK:=headers/hdrck.exe +FRAMAC_HDRCK:=tools/hdrck/hdrck.exe # Part that can be shared for external plugins include share/Makefile.headers diff --git a/tools/hdrck/dune-project b/tools/hdrck/dune-project index c96c6067e48..a7877e55264 100644 --- a/tools/hdrck/dune-project +++ b/tools/hdrck/dune-project @@ -22,5 +22,5 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (package - (name frama-c-hdchk) + (name frama-c-hdrck) ) -- GitLab