| changeset 44569 | 5130dfe1b7be |
| parent 44531 | bfc0bb115fa1 |
| child 44597 | 518e44a0ee15 |
| 44565:93dcfcf91484 | 44569:5130dfe1b7be |
|---|---|
136 fi |
136 fi |
137 fi |
137 fi |
138 |
138 |
139 if [ "$OUTDATED" = true ] |
139 if [ "$OUTDATED" = true ] |
140 then |
140 then |
141 echo "###" |
|
142 echo "### Building Isabelle/Scala layer ..." |
141 echo "### Building Isabelle/Scala layer ..." |
143 echo "###" |
|
144 |
142 |
145 [ "${#UPDATED[@]}" -gt 0 ] && { |
143 [ "${#UPDATED[@]}" -gt 0 ] && { |
146 echo "Changed files:" |
144 echo "Changed files:" |
147 for FILE in "${UPDATED[@]}" |
145 for FILE in "${UPDATED[@]}" |
148 do |
146 do |