From 685c8228ba7e735e8e3476489e14d71ad9db9682 Mon Sep 17 00:00:00 2001 From: Greg Lin Date: Wed, 4 Sep 2019 16:13:27 -0500 Subject: [PATCH] Set the HTTP user agent in the system Rprofile --- builder/build.sh | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/builder/build.sh b/builder/build.sh index 667b1d0..f714471 100755 --- a/builder/build.sh +++ b/builder/build.sh @@ -94,8 +94,9 @@ compile_r() { make make install - # Add OS identifier to the default HTTP user agent - cat <> /opt/R/${1}/lib/R/etc/Rprofile.site + # Add OS identifier to the default HTTP user agent. + # Set this in the system Rprofile so it works when R is run with --vanilla. + cat <> /opt/R/${1}/lib/R/library/base/R/Rprofile ## Set the default HTTP user agent local({ os_identifier <- if (file.exists("/etc/os-release")) {