Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
POTTIER Francois
menhir
Commits
69ba861d
Commit
69ba861d
authored
Feb 05, 2020
by
POTTIER Francois
Browse files
Fix [make data] to remove directory information from the [name] field.
parent
fa27bfdb
Changes
1
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
69ba861d
...
...
@@ -53,10 +53,12 @@ SED=$(shell if [[ "$$OSTYPE" == "darwin"* ]] ; then echo gsed ; else echo sed ;
data
:
test
@
echo
"Collecting data (using
$(SED)
)..."
&&
\
echo
"name,terminals,nonterminals,lr0states,lr1states,lr1time"
>
analysis/data.csv
&&
\
directory
=
_build/default/test/static/src
&&
\
successful
=
0
&&
timedout
=
0
&&
\
for
timings
in
_build/default/test/static/src
/
*
.out.timings
;
do
\
for
timings
in
$$
directory
/
*
.out.timings
;
do
\
name
=
$
${timings%.out.timings}
;
\
out
=
$$
name.out
;
\
name
=
`
basename
$$
name
`
;
\
if
grep
--quiet
"TIMEOUT after"
$$
out
;
then
\
((
timedout++
))
;
\
else
\
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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