From 0b53dc0394503249271c8d1c964ef481d9c381fc Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Fri, 12 May 2023 15:40:47 +0200 Subject: [PATCH] [tests] remove obsolete command (setting FRAMAC_PLUGIN) --- tests/pretty_printing/test_config | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/pretty_printing/test_config b/tests/pretty_printing/test_config index 5feb4989bf0..ada89b488ce 100644 --- a/tests/pretty_printing/test_config +++ b/tests/pretty_printing/test_config @@ -2,5 +2,4 @@ COMMENT: this directory is meant to test the parser and pretty-printer COMMENT: the default option checks that pretty-printed code can be merged COMMENT: with the original one PLUGIN: -CMD: FRAMAC_PLUGIN=tests/.empty @frama-c@ OPT: @PTEST_FILE@ -print -then -ocode ./ocode_@PTEST_NAME@.c -print -then ./ocode_@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print -- GitLab