Skip to content

Commit

Permalink
Playground: make gen_stdlib.sh POSIX-compatible (#1456)
Browse files Browse the repository at this point in the history
  • Loading branch information
sabine authored Jul 27, 2023
1 parent 0788912 commit b5eaf42
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion playground/gen_stdlib.sh
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ copylibcmis() (
srcdir=$(opam var $1:lib)
jsoo_listunits -o $tmpfile $2
for i in $(cat $tmpfile); do
cp $srcdir/?${i:1}.cmi stdlib/
cp $srcdir/?${i#?}.cmi stdlib/
done
rm $tmpfile
)
Expand Down

0 comments on commit b5eaf42

Please sign in to comment.