JSON URL fix

This commit is contained in:
Antonin Portelli 2023-01-27 12:47:05 +00:00
parent 928528ccfe
commit c9d3d0bbc5

View File

@ -2,7 +2,7 @@
set -euo pipefail set -euo pipefail
json_url='https://github.com/nlohmann/json/blob/bc889afb4c5bf1c0d8ee29ef35eaaf4c8bef8a5d/single_include/nlohmann/json.hpp' json_url='https://raw.githubusercontent.com/nlohmann/json/bc889afb4c5bf1c0d8ee29ef35eaaf4c8bef8a5d/single_include/nlohmann/json.hpp'
if [ ! -f json.hpp ]; then if [ ! -f json.hpp ]; then
wget ${json_url} wget ${json_url}