Rahel A. Fainchtein

I had tried aliasing via `alias make=/usr/local/bin/gmake` but had not had any success on that front. After trying to set $MAKE in my .bash_profile, I saw the path change in...

After checking https://www.gnu.org/software/make/manual/make.html it seems like $(MAKE_VERSION) was the culprit of the run failing. "The built-in variable ‘MAKE_VERSION’ expands to the version number of the GNU make program" I've set...

I am now running into an issue building the hacl-star portion when trying to run make. Since I am still getting familiar with the project's components I cannot tell whether...

OK - @msprotz Are the issues with hacl-star on OSX isolated to the initial build, or would I need to be prepared for persistent issues after building?

One last question - Is the OSX-specific behavior at all an issue with the Linux version? Based on @beurdouche 's response, it sounds like I may need to consider using...