On Wed, 23 Oct 2019 15:27:32 -0700 (PDT), Norman Megill <[email protected]> wrote: > David, could you see if http://173.76.107.169/index.html works for reaching > the site? That is the direct IP of us2.metamath.org. I can't test it > meaningfully because it's the IP of my house. If it works, could you > temporarily change the Travis script to retrieve the metamath program from > there?
Done. All: If you have outstanding pull requests, "git checkout develop; git pull" to sync your develop branch. Then "git checkout YOUR_BRANCH; git merge develop" to bring in the recent change to remove DNS names. Then "git push" to push out the change, which should now pass. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1iNS9y-0000XC-9Y%40rmmprod07.runbox.
