Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
b4098739
Commit
b4098739
authored
Aug 27, 2020
by
Andre Maroneze
💬
Browse files
[Makefile] add warning about weird ocp-indent + dune 2 bug
parent
3a391deb
Changes
1
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
b4098739
...
...
@@ -1790,11 +1790,14 @@ lint: $(LINT_TARGET)
check-ocp-indent-version
:
if
command
-v
ocp-indent
>
/dev/null
;
then
\
$(
eval
ocp_version_major :
=
$(
shell
ocp-indent
--version
|
$(SED)
-E
"s/^([0-9]+
)
\.
[0-9]+
\.
.*/
\1
/"
))
\
$(
eval
ocp_version_minor :
=
$(
shell
ocp-indent
--version
|
$(SED)
-E
"s/^[0-9]+
\.
([0-9]+
)
\.
.*/
\1
/"
))
\
if
[
"
$(ocp_version_major)
"
-lt
1
-o
"
$(ocp_version_minor)
"
-lt
7
]
;
then
\
echo
"error: ocp-indent >=1.7.0 required for linting (got
$(ocp_version_major)
.
$(ocp_version_minor)
)"
;
\
if
[
-z
"
$(
shell
ocp-indent --version
)
"
]
;
then
echo
"warning: ocp-indent returned an empty string, assuming it is the correct version"
;
\
else
\
$(
eval
ocp_version_major :
=
$(
shell
ocp-indent
--version
|
$(SED)
-E
"s/^([0-9]+
)
\.
[0-9]+
\.
.*/
\1
/"
))
\
$(
eval
ocp_version_minor :
=
$(
shell
ocp-indent
--version
|
$(SED)
-E
"s/^[0-9]+
\.
([0-9]+
)
\.
.*/
\1
/"
))
\
if
[
"
$(ocp_version_major)
"
-lt
1
-o
"
$(ocp_version_minor)
"
-lt
7
]
;
then
\
echo
"error: ocp-indent 1.7.0 required for linting (got
$(ocp_version_major)
.
$(ocp_version_minor)
)"
;
\
exit
1
;
\
fi
;
\
fi
;
\
else
\
exit
1
;
\
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment