Skip to content
Permalink
Browse files

Whitelist paths for refreshing hints

  • Loading branch information
s-zanella committed Nov 28, 2019
1 parent 0bfce18 commit bcd1c9d40bbb128cde9ddde9f64b4210824afe8a
Showing with 3 additions and 1 deletion.
  1. +3 −1 .docker/build/build.sh
@@ -176,7 +176,9 @@ function refresh_hints() {
echo "Current branch_name=$CI_BRANCH"

# Add all the hints, even those not under version control
find $hints_dir -iname '*.hints' | xargs git add
find $hints_dir/doc -iname '*.hints' | xargs git add
find $hints_dir/examples -iname '*.hints' | xargs git add
find $hints_dir/ulib -iname '*.hints' | xargs git add

# Without the eval, this was doing weird stuff such as,
# when $2 = "git ls-files src/ocaml-output/ | xargs git add",

0 comments on commit bcd1c9d

Please sign in to comment.
You can’t perform that action at this time.